---

Step * of Lemma peval-unroll

∀[z,v0:Top].  (peval(v0;z) ~ extend-val(v0;fix((λ%,a. extend-val(v0;%;a)));z))
BY
{ (UnivCD THENA Auto) }

1
1. z : Top
2. v0 : Top
⊢ peval(v0;z) ~ extend-val(v0;fix((λ%,a. extend-val(v0;%;a)));z)

---

Latex:

---

Latex:
\mforall{}[z,v0:Top].    (peval(v0;z)  \msim{}  extend-val(v0;fix((\mlambda{}\%,a.  extend-val(v0;\%;a)));z))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index