proposition: Lemma set_remove_1 (a b : A) (l : set) : In a (set_remove b l) -> In a l.
proof: Proof. induction l as [|x xs Hrec]. - intros. auto. - simpl. destruct (Aeq_dec b x). * tauto. * intro H. destruct H. + rewrite H. apply in_eq. + apply in_cons. apply Hrec. assumption. Qed.
imports: List