unfold CliqueFree at h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
h : ¬CliqueFree (mp M) (t + 2)
⊢ False
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
h : ¬∀ (t_1 : Finset α), ¬IsNClique (mp M) (t + 2) t_1
⊢ False