proposition: Lemma fnd_zip f1 f2 f x (v1 v2 : V) : fnd x f1 = Some v1 -> fnd x f2 = Some v2 -> zip f1 f2 = Some f -> fnd x f = zip_f v1 v2.
proof: Proof. case: f1 f2=>s1 H1 [s2 H2] /=; move: (zip_sorted' _). case E: (zip' s1 s2)=>[s|//] pf; rewrite /fnd /= => F1 F2. case=><-{f} /= {pf H1 H2}. elim: s1 s2 s E F1 F2=>[|[k1 w1] s1 IH]; case=>[|[k2 w2] s2] //= s. case: eqP=>// <-{k2}; case E1: (zip_f w1 w2)=>[w|//]. case E2: (zip' s1 s2)=>[t|//] [<-{s}]. case: eqP=>/=; last by case: eqP=>// _ _; apply: IH. by move=>->{k1}; rewrite eq_refl; case=><- [<-]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)