{α : Sort u} →
  {P : Sort u_1} →
    {rel : α → α → Prop} →
      {rel_refl : ∀ {x : α}, rel x x} →
        {rel_trans : ∀ {x y z : α}, rel x y → rel y z → rel x z} →
          {rel_antisymm : ∀ {x y : α}, rel x y → rel y x → x = y} →
            {rel' : α → α → Prop} →
              {rel_refl' : ∀ {x : α}, rel' x x} →
                {rel_trans' : ∀ {x y z : α}, rel' x y → rel' y z → rel' x z} →
                  {rel_antisymm' : ∀ {x y : α}, rel' x y → rel' y x → x = y} →
                    { rel := rel, rel_refl := rel_refl, rel_trans := rel_trans, rel_antisymm := rel_antisymm } =
                        { rel := rel', rel_refl := rel_refl', rel_trans := rel_trans', rel_antisymm := rel_antisymm' } →
                      (rel ≍ rel' → P) → P