no goals
α✝ : Type u_1
a b : α✝
l : List α✝
h : a ∈ b :: l
⊢ a = b ∨ a ∈ l
cases h <;> simp [Membership.mem, *]
no goals
α✝ : Type u_1
a b : α✝
l : List α✝
⊢ a ∈ a :: l
constructor
case a
α✝ : Type u_1
a b✝ : α✝
l : List α✝
b : α✝
h : a ∈ l
⊢ Mem a l
α✝ : Type u_1
a b✝ : α✝
l : List α✝
b : α✝
h : a ∈ l
⊢ a ∈ b :: l
constructor
no goals
case a
α✝ : Type u_1
a b✝ : α✝
l : List α✝
b : α✝
h : a ∈ l
⊢ Mem a l
assumption