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` THEN RepUR ``in-eclass es-interface-count`` 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