proposition: Lemma mem_1 : forall m (Hm:NoDupA m) x, In x m -> mem x m = true.
proof: Proof. intros m Hm x; generalize Hm; clear Hm. induction m; simpl; intros NoDup belong1. - inversion belong1. inversion H. - destruct a; destruct X.eq_dec; [reflexivity|]; apply IHm. + inversion_clear NoDup; assumption. + inversion_clear belong1; inversion_clear H; [elim n; apply H0|exists x0; auto]. Qed.
imports: FMapInterface