∀ {n : ℕ} {F : TypeVec.{u_1} (n + 1) → Type u_1} [q : MvQPF F] {α : TypeVec.{u_1} n} {β : MvQPF.Fix F α → Type u_1}
  (g : (x : F (α ::: Sigma β)) → β (MvQPF.Fix.mk (MvFunctor.map (TypeVec.id ::: Sigma.fst) x))) (x : MvQPF.Fix F α),
  x = (MvQPF.Fix.rec (fun i => ⟨MvQPF.Fix.mk (MvFunctor.map (TypeVec.id ::: Sigma.fst) i), g i⟩) x).fst →
    β (MvQPF.Fix.rec (fun i => ⟨MvQPF.Fix.mk (MvFunctor.map (TypeVec.id ::: Sigma.fst) i), g i⟩) x).fst = β x