proposition: Lemma set_remove_3 (a b : A) (l : set) : In a l -> a <> b -> In a (set_remove b l).
proof: Proof. induction l as [|x xs Hrec]. - now simpl. - simpl. destruct (Aeq_dec b x) as [<-|Hbx]; simpl; intuition. congruence. Qed.
imports: List