---

Step * of Lemma equipollent-sum-zero

∀[A:Type]. (A + ℕ0 ~ A ∧ ℕ0 + A ~ A)
BY
{ Auto }

1
1. [A] : Type
⊢ A + ℕ0 ~ A

2
1. [A] : Type
2. A + ℕ0 ~ A
⊢ ℕ0 + A ~ A

---

Latex:

---

Latex:
\mforall{}[A:Type].  (A  +  \mBbbN{}0  \msim{}  A  \mwedge{}  \mBbbN{}0  +  A  \msim{}  A)


By

---

Latex:
Auto

---

Home Index