---

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


1. T : Type
2. ∀[x:Base]. (x)↓ supposing x ∈ T
3. x : T
⊢ (x)↓
BY
{ PointwiseFunctionality 3 }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
PointwiseFunctionality  3

---

Home Index