proposition: Lemma mapf_fcat s1 s2 : mapf (fcat s1 s2) = fcat (mapf s1) (mapf s2).
proof: Proof. elim/fmap_ind': s2 s1=>[|k v s2 H IH] s1 /=. - rewrite fcats0; set j := FinMap _. by rewrite (_ : j = nil K V) ?fcat0s //; apply/fmapE. by rewrite fcat_sins mapf_ins IH -fcat_sins mapf_ins. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)