---

Step * 1 2 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. ∃G:ℕ∞ ⟶ Type. ((∀n:ℕ. G n∞ ~ ℕ1) ∧ G ∞ ~ ℕ0)
⊢ ∃G:ℕ∞ ⟶ Type. ((∀n:ℕ. G n∞ ~ F n) ∧ G ∞ ~ T)
BY
{ (ExRepD THEN RenameVar `unit_to_void' (-3) THEN (InstLemma `nat-inf-attach-unit` [⌜F⌝]⋅ THENA Auto) THEN ExRepD) }

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
⊢ ∃G:ℕ∞ ⟶ Type. ((∀n:ℕ. G n∞ ~ F n) ∧ G ∞ ~ 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.  \mexists{}G:\mBbbN{}\minfty{}  {}\mrightarrow{}  Type.  ((\mforall{}n:\mBbbN{}.  G  n\minfty{}  \msim{}  \mBbbN{}1)  \mwedge{}  G  \minfty{}  \msim{}  \mBbbN{}0)
\mvdash{}  \mexists{}G:\mBbbN{}\minfty{}  {}\mrightarrow{}  Type.  ((\mforall{}n:\mBbbN{}.  G  n\minfty{}  \msim{}  F  n)  \mwedge{}  G  \minfty{}  \msim{}  T)


By

---

Latex:
(ExRepD
  THEN  RenameVar  `unit\_to\_void'  (-3)
  THEN  (InstLemma  `nat-inf-attach-unit`  [\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index