---

Step * of Lemma natrec-unroll

∀[g,n:Top].  (letrec f(n)=g[n;f] in f n ~ g[n;letrec f(n)=g[n;f] in f])
BY
{ (Auto THEN Unfold `natrec` 0 THEN RW (AddrC [1] (RecUnfoldC `genrec`)) 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g,n:Top].    (letrec  f(n)=g[n;f]  in  f  n  \msim{}  g[n;letrec  f(n)=g[n;f]  in  f])


By

---

Latex:
(Auto  THEN  Unfold  `natrec`  0  THEN  RW  (AddrC  [1]  (RecUnfoldC  `genrec`))  0  THEN  Reduce  0  THEN  Auto)

---

Home Index