α : Type u_1
β : Type ?u.25331
γ : Type ?u.25334
a : α
⊢ a ∈ a ::ₘ 0
α : Type u_1
β : Type ?u.25331
γ : Type ?u.25334
a : α
⊢ a ∈ {a}
rw [← cons_zero]
no goals
α : Type u_1
β : Type ?u.25331
γ : Type ?u.25334
a : α
⊢ a ∈ a ::ₘ 0
exact mem_cons_self _ _