---

Step * of Lemma has-valueall-lambda

∀[a:Base]. has-valueall(λx.a[x])
BY
{ (Auto THEN UnfoldTopAb 0 THEN RecUnfold `evalall` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:Base].  has-valueall(\mlambda{}x.a[x])


By

---

Latex:
(Auto  THEN  UnfoldTopAb  0  THEN  RecUnfold  `evalall`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index