proposition: Lemma combine_NoDup : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'), NoDupA (@eqk oee') (combine m m').
proof: Proof. unfold combine, combine_r, combine_l. intros. set (f1 := fun (k : key) (e : elt) => (Some e, find k m')). set (f2 := fun (k : key) (e' : elt') => (find k m, Some e')). generalize (mapi_NoDup Hm f1). generalize (mapi_NoDup Hm' f2). set (l := mapi f1 m); clearbody l. set (r := mapi f2 m'); clearbody r. auto. Qed.
imports: FMapInterface