{α : Type u} →
  {P : Sort u_1} →
    {toPreorderPackage : Std.PreorderPackage α} →
      {toOrd : Ord α} →
        {toLawfulOrderOrd : Std.LawfulOrderOrd α} →
          {le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a} →
            {toPreorderPackage' : Std.PreorderPackage α} →
              {toOrd' : Ord α} →
                {toLawfulOrderOrd' : Std.LawfulOrderOrd α} →
                  {le_total' : ∀ (a b : α), a ≤ b ∨ b ≤ a} →
                    { toPreorderPackage := toPreorderPackage, toOrd := toOrd, toLawfulOrderOrd := toLawfulOrderOrd,
                          le_total := le_total } =
                        { toPreorderPackage := toPreorderPackage', toOrd := toOrd',
                          toLawfulOrderOrd := toLawfulOrderOrd', le_total := le_total' } →
                      (toPreorderPackage ≍ toPreorderPackage' → toOrd ≍ toOrd' → P) → P