proposition: Lemma set_union_elim : forall (a:A) (x y:set), set_In a (set_union x y) -> set_In a x \/ set_In a y.
proof: Proof. simple induction y; simpl. - auto with datatypes. - intros. generalize (set_add_elim _ _ _ H0). intros [H1| H1]. + auto with datatypes. + tauto. Qed.
imports: List