{α : Type u} →
  {inst : LE α} →
    {P : Sort u_1} →
      {toOrderTop : OrderTop α} →
        {toOrderBot : OrderBot α} →
          {toOrderTop' : OrderTop α} →
            {toOrderBot' : OrderBot α} →
              { toOrderTop := toOrderTop, toOrderBot := toOrderBot } =
                  { toOrderTop := toOrderTop', toOrderBot := toOrderBot' } →
                (toOrderTop ≍ toOrderTop' → toOrderBot ≍ toOrderBot' → P) → P