∀
  (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 + 1)) (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) (i : Fin2 n)
  (x : TypeVec.Subtype_ p i.fs)
  (h_1 :
    (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)
  (h_2 :
    (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),
  (match n + 1, α, p, i.fs, x with
    | .(n + 1), α, p, i.fs, x => h_1 n α p i x
    | .(n + 1), α, p, Fin2.fz, x => h_2 n α p x) =
    h_1 n α p i x