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