∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_2} n} {C : Type u_1}
  (g : (a : P.A) → (f : P.last.B a → P.last.W) → TypeVec.Arrow (P.WPath (WType.mk a f)) α → (P.last.B a → C) → C)
  (a : P.A) (f : P.last.B a → P.last.W) (f' : TypeVec.Arrow (P.WPath (WType.mk a f)) α),
  P.wpRec g (WType.mk a f) f' = g a f f' fun i => P.wpRec g (f i) (P.wPathDestRight f' i)