proposition: Lemma zip_supp' s1 s2 s : zip' s1 s2 = Some s -> map key s = map key s1.
proof: Proof. elim: s1 s2 s=>[|[k1 v1] s1 IH] /=; first by case=>// s [<-]. case=>[|[k2 v2] s2] // s; case: eqP=>// ->{k1}. case E: (zip_f v1 v2)=>[w|//]; case F: (zip' s1 s2)=>[t|//]. by move/IH: F=><- [<-]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)