∀
  (motive :
    (n : ℕ) →
      (α : TypeVec.{u_1} n) →
        (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) →
          (x : Fin2 n) → { x_1 // TypeVec.ofRepeat (p x (TypeVec.prod.mk x x_1.1 x_1.2)) } → Sort u_2)
  (n : ℕ) (α : TypeVec.{u_1} (n + 1)) (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop))
  (x : { x // TypeVec.ofRepeat (p Fin2.fz (TypeVec.prod.mk Fin2.fz x.1 x.2)) })
  (h_1 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop)) →
          (i : Fin2 n) →
            (x : { x // TypeVec.ofRepeat (p i.fs (TypeVec.prod.mk i.fs x.1 x.2)) }) → motive (n + 1) α p i.fs x)
  (h_2 :
    (n : ℕ) →
      (α : TypeVec.{u_1} (n + 1)) →
        (p : (α.prod α).Arrow (TypeVec.repeat (n + 1) Prop)) →
          (x : { x // TypeVec.ofRepeat (p Fin2.fz (TypeVec.prod.mk Fin2.fz x.1 x.2)) }) → motive (n + 1) α p Fin2.fz x),
  (match n + 1, α, p, Fin2.fz, 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_2 n α p x