exact ⟨B, h2⟩
case intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U B : Finset α
left✝ : B ⊆ U
h2 : IsNClique G s B
⊢ ∃ t, IsNClique G s t
no goals