Step * of Lemma value-type_functionality

[T,T':Type].  value-type(T) ⇐⇒ value-type(T') supposing T ≡ T'
BY
(Unfold `value-type` 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