{n : ℕ} →
  {P : MvPFunctor.{u} (n + 1)} →
    {motive : (a : P.last.W) → (a_1 : Fin2 n) → P.WPath a a_1 → Sort u_1} →
      {a : P.last.W} →
        {a_1 : Fin2 n} →
          (t : P.WPath a a_1) →
            t.ctorIdx = 0 →
              ((a : P.A) →
                  (f : P.last.B a → P.last.W) →
                    (i : Fin2 n) → (c : P.drop.B a i) → motive (WType.mk a f) i (MvPFunctor.WPath.root a f i c)) →
                motive a a_1 t