rintro g - hg h
case empty

⊢ ∀ {g : Multiset ℕ}, (∀ x ∈ 0, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → Multiset.prod 0 = g.prod → 0 = g
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : Multiset.prod 0 = g.prod
⊢ 0 = g