proposition: Lemma zip_unitE' s1 s2 : (exists s, zip' s1 s2 = Some s) <-> zip_unit' s1 = zip_unit' s2.
proof: Proof. split. - case; elim: s1 s2 =>[|[k1 v1] s1 IH]; case=>// [[k2 v2] s2] s //=. case: eqP=>// <-{k2}. case E1: (zip_f v1 v2)=>[w|//]; case E2: (zip' s1 s2)=>[t|//] _. by move/IH: E2=>->; congr ((_, _)::_); apply/unitE; exists w. elim: s1 s2=>[|[k1 v1] s1 IH]; case=>//; first by exists [::]. case=>k2 v2 s2 //= [<-{k2}]; case/unitE=>s ->; case/IH=>t ->. by exists ((k1, s)::t); rewrite eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)