---

Step * 1 2 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. unit_to_void : ℕ∞ ⟶ Type
7. ∀n:ℕ. unit_to_void n∞ ~ ℕ1
8. unit_to_void ∞ ~ ℕ0
9. G : ℕ∞ ⟶ Type
10. ∀n:ℕ. G n∞ ~ F n
11. G ∞ ~ ℕ1
⊢ (∀n:ℕ. G n∞ × (unit_to_void n∞) + (T × (void_to_unit n∞)) ~ F n) ∧ G ∞ × (unit_to_void ∞) + (T × (void_to_unit ∞)) ~ T
BY
{ ((RWW "4 5 7 8 10 11 equipollent-multiply equipollent-product-one.1" 0 THENA Auto) THEN Reduce 0) }

1
1. F : ℕ ⟶ Type
2. T : Type
3. void_to_unit : ℕ∞ ⟶ Type
4. ∀n:ℕ. void_to_unit n∞ ~ ℕ0
5. void_to_unit ∞ ~ ℕ1
6. unit_to_void : ℕ∞ ⟶ Type
7. ∀n:ℕ. unit_to_void n∞ ~ ℕ1
8. unit_to_void ∞ ~ ℕ0
9. G : ℕ∞ ⟶ Type
10. ∀n:ℕ. G n∞ ~ F n
11. G ∞ ~ ℕ1
⊢ (∀n:ℕ. F n + (T × ℕ0) ~ F n) ∧ ℕ0 + T ~ T

---

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.  unit\_to$_{void}$  :  \mBbbN{}\minfty{}  {}\mrightarrow{}  Type
7.  \mforall{}n:\mBbbN{}.  unit\_to$_{void}$  n\minfty{}  \msim{}  \mBbbN{}1
8.  unit\_to$_{void}$  \minfty{}  \msim{}  \mBbbN{}0
9.  G  :  \mBbbN{}\minfty{}  {}\mrightarrow{}  Type
10.  \mforall{}n:\mBbbN{}.  G  n\minfty{}  \msim{}  F  n
11.  G  \minfty{}  \msim{}  \mBbbN{}1
\mvdash{}  (\mforall{}n:\mBbbN{}.  G  n\minfty{}  \mtimes{}  (unit\_to$_{void}$  n\minfty{})  +  (T  \mtimes{}  (void\_to$_{unit}\mbackslash{}ff\000C24  n\minfty{}))  \msim{}  F  n)
\mwedge{}  G  \minfty{}  \mtimes{}  (unit\_to$_{void}$  \minfty{})  +  (T  \mtimes{}  (void\_to$_{unit}$  \minfty{}))  \msim{}  \000CT


By

---

Latex:
((RWW  "4  5  7  8  10  11  equipollent-multiply  equipollent-product-one.1"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index