no goals
ι : Sort ?u.137668
𝕜 : Type ?u.137671
V : Type u
W : Type v
X : Type w
G : SimpleGraph V
G' : SimpleGraph W
a b c u v✝ w✝ : V
e : Sym2 V
v w : V
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ incidenceSet G v ↔ Adj G v w
simp [incidenceSet]