proposition: Lemma lem_sets_2 : (forall A B X, In X (Sum A B) <-> In X A \/ In X B) /\ (forall A B, Seteq A B <-> Subset A B /\ Subset B A) /\ (forall A B, Subset A B <-> forall X, In X A -> In X B) -> (forall A, Seteq (Sum A A) A).
proof: Proof. hauto. Qed.
imports: Hammer(Tactics) Arith ZArith