proposition: Lemma zipA' s1 s2 s3 : obind (zip' s1) (zip' s2 s3) = obind (zip'^~ s3) (zip' s1 s2).
proof: Proof. elim: s1 s2 s3=>[|[k1 v1] s1 IH]. - case=>[|[k2 v2] s2]; case=>[|[k3 v3] s3] //=; case: eqP=>// ->{k2}. by case: (zip_f v2 v3)=>// v; case: (zip' s2 s3). case=>[|[k2 v2] s2]; case=>[|[k3 v3] s3] //=. - by case: eqP=>// ->{k1}; case: (zip_f v1 v2)=>// v; case: (zip' s1 s2). case: (k2 =P k3)=>[->{k2}|E1] /=; last first. - case: (k1 =P k2)=>E2 //=. case: (zip_f v1 v2)=>// v. case: (zip' s1 s2)=>//= s. by rewrite E2; case: eqP E1. case: (k1 =P k3)=>[->{k1}|E1] /=; last first. - by case: (zip_f v2 v3)=>// v; case: (zip' s2 s3)=>//= s; case: eqP E1. case E1: (zip_f v2 v3)=>[w1|]; last first. - case E3: (zip_f v1 v2)=>[w3|] //. case S3: (zip' s1 s2)=>[t3|] //=; rewrite eq_refl. by move: (assoc v1 v2 v3); rewrite /obind/oapp E1 E3=><-. case S1: (zip' s2 s3)=>[t1|] /=; last first. - case E3: (zip_f v1 v2)=>[w3|//]. case S3: (zip' s1 s2)=>[t3|] //=; rewrite eq_refl. move: (IH s2 s3); rewrite /obind/oapp S1 S3=><-. by case: (zip_f w3 v3). rewrite eq_refl. case E3: (zip_f v1 v2)=>[w3|]; move: (assoc v1 v2 v3); rewrite /obind/oapp E1 E3=>-> //=. case S3: (zip' s1 s2)=>[t3|]; move: (IH s2 s3); rewrite /obind/oapp S3 S1=>-> /=. - by rewrite eq_refl. by case: (zip_f w3 v3). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)