proposition: Lemma zip_unitE f1 f2 : (exists f, zip f1 f2 = Some f) <-> zip_unit f1 = zip_unit f2.
proof: Proof. case: f1 f2=>s1 H1 [s2 H2] /=; split. - case=>s; move: (zip_sorted' _). case E: (zip' s1 s2)=>[t|//] _ _; apply/fmapE=>/=. by apply/zip_unitE'; exists t. case; case/zip_unitE'=>s E; move/(zip_sorted' H1): (E)=>T. exists (FinMap T); move: (zip_sorted' _); rewrite E=>pf. by congr Some; apply/fmapE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)