---

Step * of Lemma es-interface-count-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].  #X(e) ~ ||≤(X)(e)|| supposing ↑e ∈b X
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN Unfold `eclass` 3
   THEN RepUR ``eclass-val in-eclass es-interface-count`` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].    \#X(e)  \msim{}  ||\mleq{}(X)(e)||  supposing  \muparrow{}e  \mmember{}\msubb{}  X


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  Unfold  `eclass`  3
  THEN  RepUR  ``eclass-val  in-eclass  es-interface-count``  0
  THEN  AutoSplit)

---

Home Index