---

Step * of Lemma eo-forward-header

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

---

Latex:

---

Latex:
\mforall{}[es,e,e':Top].    (header(e')  \msim{}  header(e'))


By

---

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

---

Home Index