proposition: Lemma zipC' s1 s2 : zip' s1 s2 = zip' s2 s1.
proof: Proof. elim: s1 s2=>[|[k1 v1] s1 IH]; first by case=>//; case. case=>[|[k2 v2] s2] //=; rewrite eq_sym; case: eqP=>// ->{k2}. by rewrite comm IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)