intro x hx y hy hne
α : 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
⊢ IsClique G (insert v ↑B)
α : 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 : α
hx : x ∈ insert v ↑B
y : α
hy : y ∈ insert v ↑B
hne : x ≠ y
⊢ Adj G x y