proposition: Lemma set_add_nodup a l : NoDup l -> NoDup (set_add a l).
proof: Proof. induction 1 as [|x l H H' IH]; simpl. - constructor; [ tauto | constructor ]. - destruct (Aeq_dec a x) as [<-|Hax]; constructor; trivial. rewrite set_add_iff. intuition. Qed.
imports: List