intro v hv
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
⊢ ∀ (v : α), v ∈ A → degRes G v A = 0
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : CliqueFreeSet A 2
v : α
hv : v ∈ A
⊢ degRes G v A = 0