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