{α : Type u} →
  {P : Sort u_1} →
    {toLE : LE α} →
      {toLT : LT α} →
        {toBEq : BEq α} →
          {toLawfulOrderLT : Std.LawfulOrderLT α} →
            {toLawfulOrderBEq : Std.LawfulOrderBEq α} →
              {toIsPreorder : Std.IsPreorder α} →
                {decidableLE : DecidableLE α} →
                  {decidableLT : DecidableLT α} →
                    {toLE' : LE α} →
                      {toLT' : LT α} →
                        {toBEq' : BEq α} →
                          {toLawfulOrderLT' : Std.LawfulOrderLT α} →
                            {toLawfulOrderBEq' : Std.LawfulOrderBEq α} →
                              {toIsPreorder' : Std.IsPreorder α} →
                                {decidableLE' : DecidableLE α} →
                                  {decidableLT' : DecidableLT α} →
                                    { toLE := toLE, toLT := toLT, toBEq := toBEq, toLawfulOrderLT := toLawfulOrderLT,
                                          toLawfulOrderBEq := toLawfulOrderBEq, toIsPreorder := toIsPreorder,
                                          decidableLE := decidableLE, decidableLT := decidableLT } =
                                        { toLE := toLE', toLT := toLT', toBEq := toBEq',
                                          toLawfulOrderLT := toLawfulOrderLT', toLawfulOrderBEq := toLawfulOrderBEq',
                                          toIsPreorder := toIsPreorder', decidableLE := decidableLE',
                                          decidableLT := decidableLT' } →
                                      (toLE ≍ toLE' →
                                          toLT ≍ toLT' →
                                            toBEq ≍ toBEq' →
                                              decidableLE ≍ decidableLE' → decidableLT ≍ decidableLT' → P) →
                                        P