proposition: Lemma map2_NoDup : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'), NoDupA (@eqk elt'') (map2 m m').
proof: Proof. intros. unfold map2. assert (H0:=combine_NoDup Hm Hm'). set (l0:=combine m m') in *; clearbody l0. set (f':= fun p : oee' => f (fst p) (snd p)). assert (H1:=map_NoDup (elt' := option elt'') H0 f'). set (l1:=map f' l0) in *; clearbody l1. clear f' f H0 l0 Hm Hm' m m'. induction l1. - simpl; auto. - inversion_clear H1. destruct a; destruct o; simpl; auto. constructor; auto. contradict H. clear IHl1. induction l1. + inversion H. + inversion_clear H0. destruct a; destruct o; simpl in *; auto. inversion_clear H; auto. Qed.
imports: FMapInterface