simp [Fintype.card_subtype, Finset.card_univ, hs]
case h
α : Type
hde : DecidableEq α
hft : Fintype α
hs : Fintype.card α = 0
N : ℕ
hN : 1 ≤ 1
⊢ (Finset α → Finset α → Color.red = Color.red → Color.red = Color.red) ∧
    Fintype.card { a // Color.red = Color.red } = 1
no goals