---

Step * of Lemma genrec-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 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  RW  (AddrC  [1]  (RecUnfoldC  `genrec`))  0    THEN  Reduce  0  THEN  Auto)

---

Home Index