rw [List.getLast_eq_get, List.get_map, List.get_enum]
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ (List.map (Function.uncurry f) l.enum).getLast ⋯ = f l.dropLast.length (l.getLast h2)
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ Function.uncurry f
      (↑⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩,
        l.get (Fin.cast ⋯ ⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩)) =
    f l.dropLast.length (l.getLast h2)