congr
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ f (l.length - 1) (l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩)) = f (l.length - 1) (l.getLast h2)
case e_a
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩) = l.getLast h2