(motive : (x : ℕ) → (x_1 : TypeVec.{u_1} x) → x_1.Arrow (TypeVec.repeat x Prop) → Fin2 x → Sort u_2) →
  (x : ℕ) →
    (x_1 : TypeVec.{u_1} x) →
      (x_2 : x_1.Arrow (TypeVec.repeat x Prop)) →
        (x_3 : Fin2 x) →
          ((n : ℕ) →
              (x : TypeVec.{u_1} n.succ) →
                (x_4 : x.Arrow (TypeVec.repeat n.succ Prop)) → (i : Fin2 n) → motive n.succ x x_4 i.fs) →
            ((n : ℕ) →
                (x : TypeVec.{u_1} n.succ) →
                  (x_4 : x.Arrow (TypeVec.repeat n.succ Prop)) → motive n.succ x x_4 Fin2.fz) →
              motive x x_1 x_2 x_3