∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β)
  (x : (MvQPF.P F).W α),
  MvQPF.recF g x = g (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.recF g) ((MvQPF.P F).wDest' x)))