proposition: Lemma set_diff_intro : forall (a:A) (x y:set), set_In a x -> ~ set_In a y -> set_In a (set_diff x y).
proof: Proof. simple induction x. - simpl; tauto. - simpl; intros a0 l Hrec y [Ha0a| Hal] Hay. + rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay). elim (set_mem a y); [ intro Habs; discriminate Habs | auto with datatypes ]. + elim (set_mem a0 y); auto with datatypes. Qed.
imports: List