proposition: Lemma mem_2 : forall m (Hm:NoDupA m) x, mem x m = true -> In x m.
proof: Proof. intros m Hm x; generalize Hm; clear Hm; unfold PX.In,PX.MapsTo. induction m; intros NoDup hyp; try discriminate; simpl in *. destruct a, X.eq_dec. + exists e; constructor; split; [assumption|reflexivity]. + destruct IHm as [e' He']. - inversion_clear NoDup; assumption. - assumption. - exists e'; auto. Qed.
imports: FMapInterface