fact: Fixpoint zip' (s1 s2 : seq (K * V)) := match s1, s2 with [::], [::] => Some [::] | (k1, v1)::s1', (k2, v2)::s2' => if k1 == k2 then if zip_f v1 v2 is Some v then if zip' s1' s2' is Some s' then Some ((k1, v) :: s') else None else None else None | _, _ => None end.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)