no goals
α : Type u_1
β : Type ?u.16480
γ : Type ?u.16483
ι : Type ?u.16486
ι' : Type ?u.16489
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ Set.Pairwise univ r ↔ Pairwise r
simp only [Set.Pairwise, Pairwise, mem_univ, forall_const]