simp only [← disjoint_edgeSet, Set.disjoint_left, Sym2.forall, mem_edgeSet]
V : Type u_1
V' : Type u_2
G✝ : SimpleGraph V
K : Type u_3
K' : Type u_4
G H : SimpleGraph V
⊢ Disjoint G H ↔ ∀ (x y : V), Adj G x y → ¬Adj H x y
no goals