---

Step * of Lemma eo-strict-forward-E-subtype

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E].  (E ⊆r E)
BY
{ (Auto
   THEN RepUR ``es-E eo-strict-forward eo-restrict`` 0
   THEN Folds ``es-base-E es-dom`` 0
   THEN D 0
   THEN Auto
   THEN ((MemTypeCD THEN Folds ``es-base-E es-dom`` 0) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].    (E  \msubseteq{}r  E)


By

---

Latex:
(Auto
  THEN  RepUR  ``es-E  eo-strict-forward  eo-restrict``  0
  THEN  Folds  ``es-base-E  es-dom``  0
  THEN  D  0
  THEN  Auto
  THEN  ((MemTypeCD  THEN  Folds  ``es-base-E  es-dom``  0)  THEN  Auto)\mcdot{})

---

Home Index