---

Step * of Lemma nat-inf-attach

∀F:ℕ ⟶ Type. ∀T:Type.  ∃G:ℕ∞ ⟶ Type. ((∀n:ℕ. G n∞ ~ F n) ∧ G ∞ ~ T)
BY
{ (Auto
   THEN (InstLemma `nat-inf-attach-unit` [⌜λn.ℕ0⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN All Reduce
   THEN RenameVar `void_to_unit' (-3)) }

1
1. F : ℕ ⟶ Type
2. T : Type
3. void_to_unit : ℕ∞ ⟶ Type
4. ∀n:ℕ. void_to_unit n∞ ~ ℕ0
5. void_to_unit ∞ ~ ℕ1
⊢ ∃G:ℕ∞ ⟶ Type. ((∀n:ℕ. G n∞ ~ F n) ∧ G ∞ ~ T)

---

Latex:

---

Latex:
\mforall{}F:\mBbbN{}  {}\mrightarrow{}  Type.  \mforall{}T:Type.    \mexists{}G:\mBbbN{}\minfty{}  {}\mrightarrow{}  Type.  ((\mforall{}n:\mBbbN{}.  G  n\minfty{}  \msim{}  F  n)  \mwedge{}  G  \minfty{}  \msim{}  T)


By

---

Latex:
(Auto
  THEN  (InstLemma  `nat-inf-attach-unit`  [\mkleeneopen{}\mlambda{}n.\mBbbN{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  All  Reduce
  THEN  RenameVar  `void\_to\_unit'  (-3))

---

Home Index