---

Step * 1 of Lemma equipollent-product-zero


1. [A] : Type
⊢ A × ℕ0 ~ ℕ0
BY
{ (With ⌜λx.x⌝ (D 0)⋅ THEN Auto THEN Try ((D -1 THEN Auto))) }

1
1. [A] : Type
⊢ Bij(A × ℕ0;ℕ0;λx.x)

---

Latex:

---

Latex:

1.  [A]  :  Type
\mvdash{}  A  \mtimes{}  \mBbbN{}0  \msim{}  \mBbbN{}0


By

---

Latex:
(With  \mkleeneopen{}\mlambda{}x.x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  Try  ((D  -1  THEN  Auto)))

---

Home Index