no goals
ι : Sort ?u.102767
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : Subgraph G
a b : V
⊢ ∀ (x y : V), Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet ⊥ ↔ Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ ∅
simp