intro g hf hg hfg
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
⊢ ∀ {g : Multiset ℕ},
    (∀ x ∈ p ::ₘ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → (p ::ₘ f).prod = g.prod → p ::ₘ f = g
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
⊢ p ::ₘ f = g