apply ih _ _ _
case cons.e_s
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
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ f = g.erase p
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
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ ∀ x ∈ f, OddPrimeOrFour x

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
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ ∀ x ∈ g.erase p, OddPrimeOrFour x

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
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ f.prod = (g.erase p).prod