∀ {α : Type u_2} {β : Type u_1} (r : Setoid α) (s : Setoid β) (x y : α × β),
  (r.prod s) x y →
    ((fun xy => (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) x).2 =
      ((fun xy => (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) y).2