{n : ℕ} →
  (P : MvPFunctor.{u_1} (n + 1)) →
    {β : Type u_2} →
      (g₀ : β → P.A) →
        (g₂ : (b : β) → P.last.B (g₀ b) → β) →
          (b : β) →
            (motive :
                (x : P.last.M) →
                  (x_1 : Fin2 n) → MvPFunctor.M.Path P x x_1 → x = MvPFunctor.M.corecShape P g₀ g₂ b → Sort u_3) →
              (x : P.last.M) →
                (x_1 : Fin2 n) →
                  (x_2 : MvPFunctor.M.Path P x x_1) →
                    (h : x = MvPFunctor.M.corecShape P g₀ g₂ b) →
                      ((x : P.last.M) →
                          (i : Fin2 n) →
                            (a : P.A) →
                              (f : P.last.B a → P.last.M) →
                                (h' : x.dest = ⟨a, f⟩) →
                                  (c : P.drop.B a i) →
                                    (h : x = MvPFunctor.M.corecShape P g₀ g₂ b) →
                                      motive x i (MvPFunctor.M.Path.root x a f h' i c) h) →
                        ((x : P.last.M) →
                            (i : Fin2 n) →
                              (a : P.A) →
                                (f : P.last.B a → P.last.M) →
                                  (h' : x.dest = ⟨a, f⟩) →
                                    (j : P.last.B a) →
                                      (c : MvPFunctor.M.Path P (f j) i) →
                                        (h : x = MvPFunctor.M.corecShape P g₀ g₂ b) →
                                          motive x i (MvPFunctor.M.Path.child x a f h' j i c) h) →
                          motive x x_1 x_2 h