{α : Type u} →
  {P : Sort u_1} →
    {toPartialOrder : PartialOrder α} →
      {sup : α → α → α} →
        {le_sup_left : ∀ (a b : α), a ≤ sup a b} →
          {le_sup_right : ∀ (a b : α), b ≤ sup a b} →
            {sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → sup a b ≤ c} →
              {toPartialOrder' : PartialOrder α} →
                {sup' : α → α → α} →
                  {le_sup_left' : ∀ (a b : α), a ≤ sup' a b} →
                    {le_sup_right' : ∀ (a b : α), b ≤ sup' a b} →
                      {sup_le' : ∀ (a b c : α), a ≤ c → b ≤ c → sup' a b ≤ c} →
                        { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left,
                              le_sup_right := le_sup_right, sup_le := sup_le } =
                            { toPartialOrder := toPartialOrder', sup := sup', le_sup_left := le_sup_left',
                              le_sup_right := le_sup_right', sup_le := sup_le' } →
                          (toPartialOrder ≍ toPartialOrder' → sup ≍ sup' → P) → P