proposition: Lemma set_diff_elim2 : forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.
proof: Proof. intros a x y; elim x; simpl. - intros; contradiction. - intros a0 l Hrec. apply set_mem_ind2; auto. intros H1 H2; case (set_add_elim _ _ _ H2); intros; auto. rewrite H; trivial. Qed.
imports: List