∀ (α : Type u_1) {r s : Setoid α},
  { toFun := fun r => ⟨r.classes, ⋯⟩, invFun := fun C => Setoid.mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } r ≤
      { toFun := fun r => ⟨r.classes, ⋯⟩, invFun := fun C => Setoid.mkClasses ↑C ⋯, left_inv := ⋯, right_inv := ⋯ } s ↔
    r ≤ s