---

Step * of Lemma es-E-subtype

∀[es:EO]. strong-subtype(E;es-base-E(es))
BY
{ ((D 0 THENA Auto) THEN Unfold `es-E` 0 THEN Folds ``es-base-E es-dom`` 0 THEN Auto)⋅ }

---

Latex:


\mforall{}[es:EO].  strong-subtype(E;es-base-E(es))


By

((D  0  THENA  Auto)  THEN  Unfold  `es-E`  0  THEN  Folds  ``es-base-E  es-dom``  0  THEN  Auto)\mcdot{}

---

Home Index