---

Step * of Lemma valueall-type_functionality

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

---

Latex:

---

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


By

---

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

---

Home Index