∀ {S X₁ X₂ : Type u_1} (f : S ⟶ X₁) (g : S ⟶ X₂) (a b : X₁ ⊕ X₂),
  CategoryTheory.Limits.Types.Pushout.Rel' f g a b →
    Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) a = Quot.mk (CategoryTheory.Limits.Types.Pushout.Rel f g) b