{n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] →
      {α : TypeVec.{u} n} →
        {β : Type u} → ({X : Type u} → (MvQPF.Cofix F α → X) → (β → X) → β → F (α ::: X)) → β → MvQPF.Cofix F α