---

Step * of Lemma assert-es-eq-E

∀[the_es:EO]. ∀[e,e':E].  uiff(e = e' ∈ E;↑e = e')
BY
{ ((UnivCD THENA Auto) THEN Unfold `es-eq-E` 0 THEN RWO "deq_property<" 0⋅ THEN Auto THEN DoSubsume THEN Auto)⋅ }

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e,e':E].    uiff(e  =  e';\muparrow{}e  =  e')


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `es-eq-E`  0
  THEN  RWO  "deq\_property<"  0\mcdot{}
  THEN  Auto
  THEN  DoSubsume
  THEN  Auto)\mcdot{}

---

Home Index