proposition: Lemma fcat_inss k v s1 s2 : k \notin supp s2 -> fcat (ins k v s1) s2 = ins k v (fcat s1 s2).
proof: Proof. by case: s2=>s2 p2 H /=; apply: fcat_ins'. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)