---

Step * 2 1 of Lemma real-list-has-valueall


1. u : ℝ
2. v : ℝ List
3. has-valueall(v)
⊢ (<evalall(u), evalall(v)>)↓
BY
{ (RepUR ``has-value`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}  List
3.  has-valueall(v)
\mvdash{}  (<evalall(u),  evalall(v)>)\mdownarrow{}


By

---

Latex:
(RepUR  ``has-value``  0  THEN  Auto)

---

Home Index