---

Step * of Lemma prime-product-injection

Inj(bag(Prime);ℕ+;λb.Π(b))
BY
{ xxx((D 0 THENA Auto) THEN Reduce 0 THEN Auto)xxx }

1
1. a1 : bag(Prime)
2. a2 : bag(Prime)
3. Π(a1) = Π(a2) ∈ ℕ+
⊢ a1 = a2 ∈ bag(Prime)

---

Latex:

---

Latex:
Inj(bag(Prime);\mBbbN{}\msupplus{};\mlambda{}b.\mPi{}(b))


By

---

Latex:
xxx((D  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto)xxx

---

Home Index