{α : Type u_1} →
  (motive : List α → Std.Format → Sort u_2) →
    (x : List α) →
      (x_1 : Std.Format) →
        ((x : Std.Format) → motive [] x) →
          ((a : α) → (as : List α) → (suffix : Std.Format) → motive (a :: as) suffix) → motive x x_1