intro ht hA
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
⊢ M.t = t → M.A = univ → CliqueFree (mp M) (t + 2)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
⊢ CliqueFree (mp M) (t + 2)