---

Step * of Lemma atomic-values-evalall

∀[x:Base]. (evalall(x))↓ supposing x ∈ atomic-values()
BY
{ Auto }

1
1. x : Base
2. x ∈ atomic-values()
⊢ (evalall(x))↓

---

Latex:

---

Latex:
\mforall{}[x:Base].  (evalall(x))\mdownarrow{}  supposing  x  \mmember{}  atomic-values()


By

---

Latex:
Auto

---

Home Index