{α : Sort u} →
  {P : Sort u_1} →
    {toPartialOrder : Lean.Order.PartialOrder α} →
      {has_csup : ∀ {c : α → Prop}, Lean.Order.chain c → Exists (Lean.Order.is_sup c)} →
        {toPartialOrder' : Lean.Order.PartialOrder α} →
          {has_csup' : ∀ {c : α → Prop}, Lean.Order.chain c → Exists (Lean.Order.is_sup c)} →
            { toPartialOrder := toPartialOrder, has_csup := has_csup } =
                { toPartialOrder := toPartialOrder', has_csup := has_csup' } →
              (toPartialOrder ≍ toPartialOrder' → P) → P