∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u_1} n} {C : (x : P.last.W) → TypeVec.Arrow (P.WPath x) α → Prop},
  (∀ (a : P.A) (f : P.last.B a → P.last.W) (f' : TypeVec.Arrow (P.WPath (WType.mk a f)) α),
      (∀ (i : P.last.B a), C (f i) (P.wPathDestRight f' i)) → C (WType.mk a f) f') →
    ∀ (x : P.last.W) (f' : TypeVec.Arrow (P.WPath x) α), C x f'