proposition: Lemma map2_1bis : forall (m: t elt)(m': t elt') x (f:option elt->option elt'->option elt''), f None None = None -> find x (map2 f m m') = f (find x m) (find x m').
proof: Proof. intros. case_eq (find x m); intros. - rewrite <- H0. apply map2_1; auto with map. left; exists e; auto with map. - case_eq (find x m'); intros. + rewrite <- H0; rewrite <- H1. apply map2_1; auto. right; exists e; auto with map. + rewrite H. case_eq (find x (map2 f m m')); intros; auto with map. assert (In x (map2 f m m')) by (exists e; auto with map). destruct (map2_2 H3) as [(e0,H4)|(e0,H4)]. * rewrite (find_1 H4) in H0; discriminate. * rewrite (find_1 H4) in H1; discriminate. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface