proposition: Lemma NoDup_nodup l: NoDup (nodup l).
proof: Proof. induction l as [|a l' Hrec]; simpl. - constructor. - destruct (in_dec decA a l'); simpl. * assumption. * constructor; [ now rewrite nodup_In | assumption]. Qed.
imports: PeanoNat