ext x
case e_f.h.e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y : α
⊢ (fun x => if Adj G x y then 1 else 0) = fun w => if Adj G y w then 1 else 0
case e_f.h.e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
⊢ (if Adj G x y then 1 else 0) = if Adj G y x then 1 else 0