congr
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ card (nbhdRes G x (A \ B)) = card (filter (fun x_1 => Adj G x x_1) (A \ B))
case e_f.h.e_s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ nbhdRes G x (A \ B) = filter (fun x_1 => Adj G x x_1) (A \ B)