---

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


1. T : Type
2. t : T
3. valueall-type(T)
⊢ (t)↓
BY
{ (FLemma `valueall-type-value-type` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  t  :  T
3.  valueall-type(T)
\mvdash{}  (t)\mdownarrow{}


By

---

Latex:
(FLemma  `valueall-type-value-type`  [-1]  THEN  Auto)

---

Home Index