no goals
ι : Type ?u.43589
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
h : a ∈ head? []
⊢ a :: tail [] = []
contradiction
ι : Type ?u.43589
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
b : α
l : List α
a : α
h : b = a
⊢ a :: tail (b :: l) = b :: l
ι : Type ?u.43589
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
b : α
l : List α
a : α
h : a ∈ head? (b :: l)
⊢ a :: tail (b :: l) = b :: l
simp at h
no goals
ι : Type ?u.43589
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
b : α
l : List α
a : α
h : b = a
⊢ a :: tail (b :: l) = b :: l
simp [h]