simp [List.filter_cons, h']
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a : α
h : filter p [a] ≠ []
h' : p a = true
⊢ (filter p [a]).getLast h = [a].getLast ⋯
no goals