---

Step * 1 1 1 of Lemma nat-inf-attach


1. F : ℕ ⟶ Type
2. T : Type
3. void_to_unit : ℕ∞ ⟶ Type
4. ∀n:ℕ. void_to_unit n∞ ~ ℕ0
5. void_to_unit ∞ ~ ℕ1
6. ∀n:ℕ. (λu.((void_to_unit u) ⟶ ℕ0)) n∞ ~ ℕ1
⊢ ℕ1 ⟶ ℕ0 ~ ℕ0
BY
{ (RWO "equipollent-product" 0 THEN Auto THEN RepUR ``int-prod`` 0 THEN RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  F  :  \mBbbN{}  {}\mrightarrow{}  Type
2.  T  :  Type
3.  void\_to$_{unit}$  :  \mBbbN{}\minfty{}  {}\mrightarrow{}  Type
4.  \mforall{}n:\mBbbN{}.  void\_to$_{unit}$  n\minfty{}  \msim{}  \mBbbN{}0
5.  void\_to$_{unit}$  \minfty{}  \msim{}  \mBbbN{}1
6.  \mforall{}n:\mBbbN{}.  (\mlambda{}u.((void\_to$_{unit}$  u)  {}\mrightarrow{}  \mBbbN{}0))  n\minfty{}  \msim{}  \mBbbN{}1
\mvdash{}  \mBbbN{}1  {}\mrightarrow{}  \mBbbN{}0  \msim{}  \mBbbN{}0


By

---

Latex:
(RWO  "equipollent-product"  0  THEN  Auto  THEN  RepUR  ``int-prod``  0  THEN  RelRST  THEN  Auto)

---

Home Index