proposition: Lemma NoDup_dec (l:list A) : {NoDup l}+{~NoDup l}.
proof: Proof. Proof using A dec. induction l as [|a l IH]. - left; now constructor. - destruct (In_dec a l). + right. inversion_clear 1. tauto. + destruct IH. * left. now constructor. * right. inversion_clear 1. tauto. Qed.
imports: List Decidable