proposition: Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m').
proof: Proof. intros. unfold map2. rewrite gmap2; auto. generalize (@mem_1 _ m x) (@mem_1 _ m' x). do 2 rewrite mem_find. destruct (find x m); simpl; auto. destruct (find x m'); simpl; auto. intros. destruct H; intuition; try discriminate. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface