ι : Type ?u.41922
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x a : α
l : List α
h : a = x
⊢ a :: l = x :: tail (a :: l)
ι : Type ?u.41922
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x a : α
l : List α
h : x ∈ head? (a :: l)
⊢ a :: l = x :: tail (a :: l)
simp only [head?, Option.mem_def, Option.some_inj] at h
no goals
ι : Type ?u.41922
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x a : α
l : List α
h : a = x
⊢ a :: l = x :: tail (a :: l)
exact h ▸ rfl