∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive []) (singleton : (a : α) → motive [a])
  (cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))) (x : List α),
  List.bidirectionalRec nil singleton cons_append x =
    match x with
    | [] => nil
    | [a] => singleton a
    | a :: b :: l =>
      ⋯ ▸
        cons_append a (b :: l).dropLast ((b :: l).getLast ⋯)
          (List.bidirectionalRec nil singleton cons_append (b :: l).dropLast)