proposition: Lemma fcat_sins k v s1 s2 : fcat s1 (ins k v s2) = ins k v (fcat s1 s2).
proof: Proof. elim/fmap_ind': s2 k v s1=>[|k1 v1 s1 H1 IH k2 v2 s2] //. case: (totalP k2 k1)=>//= H2. - have H: path ord k2 (supp (ins k1 v1 s1)). - by apply: (path_supp_ins _ H2); apply: ord_path H1. by rewrite {1}/fcat seqof_ins //= fcat_ins' ?notin_path. - by rewrite IH ins_ins H2 IH ins_ins H2. have H: path ord k1 (supp (ins k2 v2 s1)) by apply: (path_supp_ins _ H2). rewrite ins_ins. case: (totalP k2 k1) H2 => // H2 _. rewrite {1}/fcat seqof_ins //= fcat_ins' ?notin_path // IH ?notin_path //. rewrite ins_ins; case: (totalP k2 k1) H2 => // H2 _; congr (ins _ _ _). by rewrite -/(fcat s2 (ins k2 v2 s1)) IH. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)