proposition: Lemma set_diff_elim1 : forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.
proof: Proof. simple induction x. - simpl; tauto. - simpl; intros a0 l Hrec y; elim (set_mem a0 y). + eauto with datatypes. + intro; generalize (set_add_elim _ _ _ H). intros [H1| H2]; eauto with datatypes. Qed.
imports: List