push_neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
h : ∃ B, B ⊆ U ∧ IsNClique G s B
⊢ ¬∀ (t : Finset α), ¬IsNClique G s t
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
U : Finset α
h : ∃ B, B ⊆ U ∧ IsNClique G s B
⊢ ∃ t, IsNClique G s t