---

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


1. F : ℕ ⟶ Type
2. n : ℕ
3. singleton-type({x:ℕ| n∞ = x∞ ∈ ℕ∞} )
⊢ (λu.(n:{n:ℕ| u = n∞ ∈ ℕ∞}  ⟶ (F n))) n∞ ~ F n
BY
{ (RenameVar `s' (-1)
   THEN ((Reduce 0 THEN InstLemma `equipollent-singleton-domain` [⌜{x:ℕ| n∞ = x∞ ∈ ℕ∞} ⌝;⌜s⌝;⌜F⌝]⋅) THENA Auto)
   ) }

1
1. F : ℕ ⟶ Type
2. n : ℕ
3. s : singleton-type({x:ℕ| n∞ = x∞ ∈ ℕ∞} )
4. u:{x:ℕ| n∞ = x∞ ∈ ℕ∞}  ⟶ (F u) ~ F (fst(s))
⊢ n:{n@0:ℕ| n∞ = n@0∞ ∈ ℕ∞}  ⟶ (F n) ~ F n

---

Latex:

---

Latex:

1.  F  :  \mBbbN{}  {}\mrightarrow{}  Type
2.  n  :  \mBbbN{}
3.  singleton-type(\{x:\mBbbN{}|  n\minfty{}  =  x\minfty{}\}  )
\mvdash{}  (\mlambda{}u.(n:\{n:\mBbbN{}|  u  =  n\minfty{}\}    {}\mrightarrow{}  (F  n)))  n\minfty{}  \msim{}  F  n


By

---

Latex:
(RenameVar  `s'  (-1)
  THEN  ((Reduce  0  THEN  InstLemma  `equipollent-singleton-domain`  [\mkleeneopen{}\{x:\mBbbN{}|  n\minfty{}  =  x\minfty{}\}  \mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{})
              THENA  Auto
              )
  )

---

Home Index