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