---

Step * 1 of Lemma equipollent-sum-zero


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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index