---

Step * of Lemma es-interface-vals-nil

∀[X,es:Top].  (X([]) ~ [])
BY
{ ((UnivCD THENA Auto) THEN RepUR ``eclass-vals`` 0⋅ THEN Auto) }

---

Latex:


\mforall{}[X,es:Top].    (X([])  \msim{}  [])


By

((UnivCD  THENA  Auto)  THEN  RepUR  ``eclass-vals``  0\mcdot{}  THEN  Auto)

---

Home Index