no goals
α : Type u_1
s : Multiset (Multiset α)
⊢ ↑card (Sections 0) = prod (map (↑card) 0)
simp
no goals
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ ⦃a : Multiset α⦄ {s : Multiset (Multiset α)},
    ↑card (Sections s) = prod (map (↑card) s) → ↑card (Sections (a ::ₘ s)) = prod (map (↑card) (a ::ₘ s))
simp (config := { contextual := true })