{α : Type u_1} →
  {β : Type u_3} →
    (motive : List α → (List α → β) → Sort u_2) →
      (x : List α) →
        (x_1 : List α → β) →
          ((x : List α → β) → motive [] x) →
            ((y : α) → (ys : List α) → (f : List α → β) → motive (y :: ys) f) → motive x x_1