{𝕆 : Type u_5} →
  {α : Type u_6} →
    {inst : Preorder 𝕆} →
      {inst_1 : Preorder α} →
        {P : Sort u} →
          {grade : α → 𝕆} →
            {grade_strictMono : StrictMono grade} →
              {covBy_grade : ∀ ⦃a b : α⦄, a ⋖ b → grade a ⋖ grade b} →
                {grade' : α → 𝕆} →
                  {grade_strictMono' : StrictMono grade'} →
                    {covBy_grade' : ∀ ⦃a b : α⦄, a ⋖ b → grade' a ⋖ grade' b} →
                      { grade := grade, grade_strictMono := grade_strictMono, covBy_grade := covBy_grade } =
                          { grade := grade', grade_strictMono := grade_strictMono', covBy_grade := covBy_grade' } →
                        (grade ≍ grade' → P) → P