---

Step * of Lemma eo-forward-info-type

∀[f,es,e,e':Top].  (es-info-type(es.e;e';f) ~ es-info-type(es;e';f))
BY
{ ((RepUR ``es-info-type`` 0 THEN (UnivCD THENA Auto)) THEN RW (SweepDnC EoForwardC) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f,es,e,e':Top].    (es-info-type(es.e;e';f)  \msim{}  es-info-type(es;e';f))


By

---

Latex:
((RepUR  ``es-info-type``  0  THEN  (UnivCD  THENA  Auto))  THEN  RW  (SweepDnC  EoForwardC)  0  THEN  Auto)

---

Home Index