∀ {α : Type u_1} {β : Type u_2} (u : SetRel α α) (v : SetRel β β) (s : Set α) (t : Set β) (x : α × β),
  (∃ a b, (a ∈ s ∧ b ∈ t) ∧ (a, x.1) ∈ u ∧ (b, x.2) ∈ v) ↔ (∃ a ∈ s, (a, x.1) ∈ u) ∧ ∃ a ∈ t, (a, x.2) ∈ v