∀ {n : ℕ} (P : MvPFunctor.{u_1} (n + 1)) {α : TypeVec.{u_1} n} (motive : ↑P (α ::: P.W α) → Sort u_2) (a : P.A)
  (f : (P.B a).Arrow (α ::: P.W α)) (h_1 : (a : P.A) → (f : (P.B a).Arrow (α ::: P.W α)) → motive ⟨a, f⟩),
  (match ⟨a, f⟩ with
    | ⟨a, f⟩ => h_1 a f) =
    h_1 a f