proposition: Lemma nodup_fixed_point (l : list A) : NoDup l -> nodup l = l.
proof: Proof. induction l as [| x l IHl]; [auto|]. intros H. simpl. destruct (in_dec decA x l) as [Hx | Hx]; rewrite NoDup_cons_iff in H. - destruct H as [H' _]. contradiction. - destruct H as [_ H']. apply IHl in H'. rewrite -> H'. reflexivity. Qed.
imports: PeanoNat