rw [hx]
case inl.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y ∈ ↑B
⊢ Adj G x y
case inl.inr
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A B : Finset α
hv : v ∈ A
hB : B ⊆ nbhdRes G v A
h : IsClique G ↑B
x y : α
hne : x ≠ y
hx : x = v
hy : y ∈ ↑B
⊢ Adj G v y