∀
  (motive :
    (x : ℕ) →
      (x_1 : TypeVec.{u_1} x) →
        (x_2 : x_1.Arrow (TypeVec.repeat x Prop)) →
          (x_3 : Fin2 x) → { x_4 // TypeVec.ofRepeat (x_2 x_3 x_4) } → Sort u_2)
  (n : ℕ) (x : TypeVec.{u_1} n.succ) (x_1 : x.Arrow (TypeVec.repeat n.succ Prop))
  (x_2 : { x // TypeVec.ofRepeat (x_1 Fin2.fz x) })
  (h_1 :
    (n : ℕ) →
      (x : TypeVec.{u_1} n.succ) →
        (p : x.Arrow (TypeVec.repeat n.succ Prop)) →
          (i : Fin2 n) → (x_3 : { x // TypeVec.ofRepeat (p i.fs x) }) → motive n.succ x p i.fs x_3)
  (h_2 :
    (n : ℕ) →
      (x : TypeVec.{u_1} n.succ) →
        (x_3 : x.Arrow (TypeVec.repeat n.succ Prop)) →
          (x_4 : { x // TypeVec.ofRepeat (x_3 Fin2.fz x) }) → motive n.succ x x_3 Fin2.fz x_4),
  (match n.succ, x, x_1, Fin2.fz, x_2 with
    | n.succ, x, p, i.fs, x_3 => h_1 n x p i x_3
    | n.succ, x, x_3, Fin2.fz, x_4 => h_2 n x x_3 x_4) =
    h_2 n x x_1 x_2