∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive [])
  (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])) (a : α) (l : List α),
  List.reverseRec nil append_singleton (a :: l) =
    ⋯ ▸ append_singleton (a :: l).dropLast ((a :: l).getLast ⋯) (List.reverseRec nil append_singleton (a :: l).dropLast)