rw [← Finset.card_empty] at h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h : 0 < s
⊢ CliqueFreeSet ∅ s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h✝ : 0 < s
h : card ∅ < s
⊢ CliqueFreeSet ∅ s

α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h : 0 < s
⊢ Type ?u.2299