---

Step * of Lemma real-list-has-valueall

∀[x:ℝ List]. has-valueall(x)
BY
{ InductionOnList }

1
has-valueall([])

2
1. u : ℝ
2. v : ℝ List
3. has-valueall(v)
⊢ has-valueall([u / v])

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}  List].  has-valueall(x)


By

---

Latex:
InductionOnList

---

Home Index