{𝕆 : Type u_5} →
  {α : Type u_6} →
    {inst : Preorder 𝕆} →
      {inst_1 : Preorder α} →
        {P : Sort u} →
          {toGradeOrder : GradeOrder 𝕆 α} →
            {isMin_grade : ∀ ⦃a : α⦄, IsMin a → IsMin (GradeOrder.grade a)} →
              {toGradeOrder' : GradeOrder 𝕆 α} →
                {isMin_grade' : ∀ ⦃a : α⦄, IsMin a → IsMin (GradeOrder.grade a)} →
                  { toGradeOrder := toGradeOrder, isMin_grade := isMin_grade } =
                      { toGradeOrder := toGradeOrder', isMin_grade := isMin_grade' } →
                    (toGradeOrder ≍ toGradeOrder' → P) → P