---

Step * of Lemma strong-subtype-bar

∀[T:Type]. (value-type(T) ⇒ strong-subtype(T;bar(T)))
BY
{ (Unfold `bar` 0 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