---

Step * of Lemma es-is-interface-map

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:Top]. ∀[e:E].
  (e ∈b es-interface-map(f;X) ~ e ∈b X ∧b (#(f X(e) e) =z 1))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``eclass es-E-interface eclass-val 
           in-eclass es-interface-map let`` 0⋅
   THEN Unfold `eclass` 3
   THEN AutoSplit
   THEN ElimBagSizeOne
   THEN Reduce 0) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:Top].  \mforall{}[e:E].
    (e  \mmember{}\msubb{}  es-interface-map(f;X)  \msim{}  e  \mmember{}\msubb{}  X  \mwedge{}\msubb{}  (\#(f  X(e)  e)  =\msubz{}  1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``eclass  es-E-interface  eclass-val 
                  in-eclass  es-interface-map  let``  0\mcdot{}
  THEN  Unfold  `eclass`  3
  THEN  AutoSplit
  THEN  ElimBagSizeOne
  THEN  Reduce  0)

---

Home Index