proposition: Lemma set_remove_2 (a b:A) (l : set) : NoDup l -> In a (set_remove b l) -> a <> b.
proof: Proof. induction l as [|x l IH]; intro ND; simpl. - tauto. - inversion_clear ND. destruct (Aeq_dec b x) as [<-|Hbx]. + congruence. + destruct 1; subst; auto. Qed.
imports: List