proposition: Lemma zip_filter' s1 s2 s x : zip' s1 s2 = Some s -> zip' (filter (predCk V x) s1) (filter (predCk V x) s2) = Some (filter (predCk V x) s).
proof: Proof. elim: s1 s2 s=>[|[k1 v1] s1 IH]; case=>[|[k2 v2] s2] //= s; first by case=><-. case: eqP=>// <-{k2}; case E1: (zip_f v1 v2)=>[a|//]. case E2: (zip' s1 s2)=>[t|//]; move/IH: E2=>E2 [<-{s}]. case: eqP=>[->{k1}|] /=; first by rewrite E2 eq_refl. by rewrite eq_refl E1 E2; case: eqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)