proposition: Lemma NoDup_list_decidable (l:list A) : NoDup l -> forall x y:A, In x l -> In y l -> decidable (x=y).
proof: Proof. Proof using A. clear dec; intros Hl; induction Hl; firstorder congruence. Qed.
imports: List Decidable