proposition: Lemma set_inter_intro : forall (a:A) (x y:set), set_In a x -> set_In a y -> set_In a (set_inter x y).
proof: Proof. simple induction x. - auto with datatypes. - simpl; intros a0 l Hrec y [Ha0a| Hal] Hy. + simpl; rewrite Ha0a. generalize (set_mem_correct1 a y). generalize (set_mem_complete1 a y). elim (set_mem a y); simpl; intros. * auto with datatypes. * absurd (set_In a y); auto with datatypes. + elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ]. Qed.
imports: List