proposition: Lemma map2_2 : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), In x (map2 m m') -> In x m \/ In x m'.
proof: Proof. intros. destruct H as (e,H). generalize (map2_0 Hm Hm' x). rewrite (find_1 (map2_NoDup Hm Hm') H). generalize (@find_2 _ m x). generalize (@find_2 _ m' x). destruct (find x m); destruct (find x m'); simpl; intros. - left; exists e0; auto. - left; exists e0; auto. - right; exists e0; auto. - discriminate. Qed.
imports: FMapInterface