(motive :
    (n : ℕ) →
      (α : TypeVec.{u_1} n) → (p : α.Arrow (TypeVec.repeat n Prop)) → (x : Fin2 n) → TypeVec.Subtype_ p x → Sort u_2) →
  (n : ℕ) →
    (α : TypeVec.{u_1} n) →
      (p : α.Arrow (TypeVec.repeat n Prop)) →
        (x : Fin2 n) →
          (x_1 : TypeVec.Subtype_ p x) →
            ((n : ℕ) →
                (α : TypeVec.{u_1} (n + 1)) →
                  (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) →
                    (i : Fin2 n) → (x : TypeVec.Subtype_ p i.fs) → motive (n + 1) α p i.fs x) →
              ((n : ℕ) →
                  (α : TypeVec.{u_1} (n + 1)) →
                    (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) →
                      (x : TypeVec.Subtype_ p Fin2.fz) → motive (n + 1) α p Fin2.fz x) →
                motive n α p x x_1