---

Step * of Lemma assert-es-eq-E-base

∀[es:EO]. ∀[e,e':es-base-E(es)].  uiff(e = e' ∈ es-base-E(es);↑e = e')
BY
{ (BasicUniformUnivCD Auto
   THEN (InstLemma `es-eq-wf-base` [⌈es⌉]⋅ THENA Auto)
   THEN Unfold `es-eq-E` 0
   THEN RWO "deq_property<" 0⋅
   THEN Auto) }

---

Latex:


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


By

(BasicUniformUnivCD  Auto
  THEN  (InstLemma  `es-eq-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `es-eq-E`  0
  THEN  RWO  "deq\_property<"  0\mcdot{}
  THEN  Auto)

---

Home Index