no goals
α : Type u_1
G H : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
n : ℕ
a b c : α
s : Finset α
⊢ cliqueFinset G n = ∅ ↔ CliqueFree G n
simp_rw [CliqueFree, eq_empty_iff_forall_not_mem, mem_cliqueFinset_iff]