---

Step * 1 1 of Lemma valueall-type-has-valueall


1. T : Type
2. ∀[x:Base]. (evalall(x))↓ supposing x ∈ T
3. x : T
⊢ has-valueall(x)
BY
{ At ⌜Type⌝ (PointwiseFunctionality 3)⋅ }

1
1. T : Type
2. ∀[x:Base]. (evalall(x))↓ supposing x ∈ T
3. [a] : Base
4. [b] : Base
5. [c] : a = b ∈ T
⊢ has-valueall(a)

2
1. T : Type
2. ∀[x:Base]. (evalall(x))↓ supposing x ∈ T
3. a : Base
4. b : Base
5. c : a = b ∈ T
⊢ has-valueall(a) = has-valueall(b) ∈ Type

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mforall{}[x:Base].  (evalall(x))\mdownarrow{}  supposing  x  \mmember{}  T
3.  x  :  T
\mvdash{}  has-valueall(x)


By

---

Latex:
At  \mkleeneopen{}Type\mkleeneclose{}  (PointwiseFunctionality  3)\mcdot{}

---

Home Index