---

Step * of Lemma value-type_functionality

∀[T,T':Type].  value-type(T) ⇐⇒ value-type(T') supposing T ≡ T'
BY
{ (Unfold `value-type` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,T':Type].    value-type(T)  \mLeftarrow{}{}\mRightarrow{}  value-type(T')  supposing  T  \mequiv{}  T'


By

---

Latex:
(Unfold  `value-type`  0  THEN  Auto)

---

Home Index