{α : Sort u_2} →
  (motive : (x : ℕ) → (Fin x → α) → Sort u_1) →
    (x : ℕ) →
      (x_1 : Fin x → α) →
        ((x : Fin 0 → α) → motive 0 x) → ((n : ℕ) → (x : Fin (n + 1) → α) → motive n.succ x) → motive x x_1