---

Step * of Lemma es-interface-or-getleft

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:EClass(Top)]. ∀[e:E].  oob-getleft((A | B)(e)) ~ A(e) supposing ↑e ∈b A
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-1)
   THEN RepUR ``eclass-val es-interface-or in-eclass eclass-compose2 oob-apply`` 0
   THEN RepeatFor 2 (AutoSplit)
   THEN RepUR ``oob-getleft`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:EClass(Top)].  \mforall{}[e:E].
    oob-getleft((A  |  B)(e))  \msim{}  A(e)  supposing  \muparrow{}e  \mmember{}\msubb{}  A


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``eclass-val  es-interface-or  in-eclass  eclass-compose2  oob-apply``  0
  THEN  RepeatFor  2  (AutoSplit)
  THEN  RepUR  ``oob-getleft``  0
  THEN  Auto)

---

Home Index