---

Step * of Lemma map-class-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(Top)]. ∀[e:E].
  (f[v] where v from X)(e) ~ f[X(e)] supposing ↑e ∈b (f[v] where v from X)
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-1)
   THEN (Unfold `eclass` -2
         THEN RepUR ``map-class es-filter-image in-eclass eclass-compose1`` 0
         THEN RepUR ``eclass-val`` 0
         THEN AutoSplit)⋅) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[f:Top].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    (f[v]  where  v  from  X)(e)  \msim{}  f[X(e)]  supposing  \muparrow{}e  \mmember{}\msubb{}  (f[v]  where  v  from  X)


By

((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (Unfold  `eclass`  -2
              THEN  RepUR  ``map-class  es-filter-image  in-eclass  eclass-compose1``  0
              THEN  RepUR  ``eclass-val``  0
              THEN  AutoSplit)\mcdot{})

---

Home Index