rw [disjoint_iff, ← ind_inter, disjoint_iff_inter_eq_empty.1 h, ind_empty]
α : Type u_1
β : Type u_2
G H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
h : Disjoint s t
⊢ Disjoint (G.ind s) (G.ind t)
no goals