proposition: Lemma mapi_NoDup : forall m (Hm : NoDupA (@eqk elt) m)(f: key->elt->elt'), NoDupA (@eqk elt') (mapi f m).
proof: Proof. induction m; simpl; auto. intros. destruct a as (x',e'). inversion_clear Hm; auto. constructor; auto. contradict H. clear IHm H0. induction m; simpl in *; auto. - inversion_clear H. - destruct a; inversion_clear H; auto. Qed.
imports: FMapInterface