---

Step * of Lemma is-interface-count

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

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `eclass`  3
  THEN  RepUR  ``in-eclass  es-interface-count``  0
  THEN  AutoSplit)

---

Home Index