Step * of Lemma strong-subtype-bar

[T:Type]. (value-type(T)  strong-subtype(T;bar(T)))
BY
(Unfold `bar` THEN EAuto 1) }


Latex:


Latex:
\mforall{}[T:Type].  (value-type(T)  {}\mRightarrow{}  strong-subtype(T;bar(T)))


By


Latex:
(Unfold  `bar`  0  THEN  EAuto  1)




Home Index