proposition: Lemma set_remove_iff (a b : A) (l : set) : NoDup l -> (In a (set_remove b l) <-> In a l /\ a <> b).
proof: Proof. split; try split. - eapply set_remove_1; eauto. - eapply set_remove_2; eauto. - destruct 1; apply set_remove_3; auto. Qed.
imports: List