proposition: Lemma map2_1 : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), In x m \/ In x m' -> find x (map2 m m') = f (find x m) (find x m').
proof: Proof. intros. rewrite map2_0; auto. destruct H as [(e,H)|(e,H)]. - rewrite (find_1 Hm H). destruct (find x m'); simpl; auto. - rewrite (find_1 Hm' H). destruct (find x m); simpl; auto. Qed.
imports: FMapInterface