proposition: Lemma set_inter_elim2 : forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.
proof: Proof. simple induction x. - simpl; tauto. - simpl; intros a0 l Hrec y. generalize (set_mem_correct1 a0 y). elim (set_mem a0 y); simpl; intros. + elim H0; [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ]. + eauto with datatypes. Qed.
imports: List