α : Type u_1
β : Type ?u.7769
r s : Setoid α
⊢ (EqvGen.Setoid fun x y => Rel r x y ∨ Rel s x y) = EqvGen.Setoid (Rel r ⊔ Rel s)
α : Type u_1
β : Type ?u.7769
r s : Setoid α
⊢ r ⊔ s = EqvGen.Setoid (Rel r ⊔ Rel s)
rw [sup_eq_eqvGen]
no goals
α : Type u_1
β : Type ?u.7769
r s : Setoid α
⊢ (EqvGen.Setoid fun x y => Rel r x y ∨ Rel s x y) = EqvGen.Setoid (Rel r ⊔ Rel s)
rfl