---

Step * of Lemma natrec_wf

∀[T:ℕ ⟶ Type]. ∀[g:n:ℕ ⟶ (m:ℕn ⟶ T[m]) ⟶ T[n]].  (letrec f(n)=g[n;f] in f ∈ n:ℕ ⟶ T[n])
BY
{ (Unfold `natrec` 0 THEN Auto THEN Assert ⌜∀n:ℕ. (letrec f(n)=g[n;f] in f  ∈ m:ℕn ⟶ T[m])⌝⋅) }

1
.....assertion..... 
1. T : ℕ ⟶ Type
2. g : n:ℕ ⟶ (m:ℕn ⟶ T[m]) ⟶ T[n]
⊢ ∀n:ℕ. (letrec f(n)=g[n;f] in f  ∈ m:ℕn ⟶ T[m])

2
1. T : ℕ ⟶ Type
2. g : n:ℕ ⟶ (m:ℕn ⟶ T[m]) ⟶ T[n]
3. ∀n:ℕ. (letrec f(n)=g[n;f] in f  ∈ m:ℕn ⟶ T[m])
⊢ letrec f(n)=g[n;f] in
   f  ∈ n:ℕ ⟶ T[n]

---

Latex:

---

Latex:
\mforall{}[T:\mBbbN{}  {}\mrightarrow{}  Type].  \mforall{}[g:n:\mBbbN{}  {}\mrightarrow{}  (m:\mBbbN{}n  {}\mrightarrow{}  T[m])  {}\mrightarrow{}  T[n]].    (letrec  f(n)=g[n;f]  in  f  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  T[n])


By

---

Latex:
(Unfold  `natrec`  0  THEN  Auto  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  (letrec  f(n)=g[n;f]  in  f    \mmember{}  m:\mBbbN{}n  {}\mrightarrow{}  T[m])\mkleeneclose{}\mcdot{})

---

Home Index