∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g : β → ↑P (α ::: β)) (x : β),
  MvPFunctor.M.dest P (MvPFunctor.M.corec P g x) = MvFunctor.map (TypeVec.id ::: MvPFunctor.M.corec P g) (g x)