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