Theorem: Collection.subset_cons (Logic/Vorspiel/Collection.lean)

State before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a : α
x : β
⊢ a ⊆ cons x a
Tactic:
simp [subset_iff, mem_cons_iff]
State after:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a : α
x : β
⊢ ∀ x_1 ∈ a, x_1 = x ∨ x_1 ∈ a

State before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a : α
x : β
⊢ ∀ x_1 ∈ a, x_1 = x ∨ x_1 ∈ a
Tactic:
tauto
State after:
no goals