ext y
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x : V
⊢ neighborSet ⊥ x = ∅
case h
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
x y : V
⊢ y ∈ neighborSet ⊥ x ↔ y ∈ ∅