---

Step * of Lemma interface-union-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[e:E].
  X+Y(e) = if e ∈b X then inl X(e) else inr Y(e)  fi  ∈ (A + B) supposing ↑e ∈b X+Y
BY
{ (Auto
   THEN Auto
   THEN (MoveToConcl (-1) THEN All (Unfold `eclass`))
   THEN RepUR ``es-interface-union eclass-compose2 in-eclass eclass-val`` 0
   THEN RepeatFor 2 ((AutoSplit THEN Try ((Auto THEN (BLemma `single-valued-bag-if-le1` THEN Auto)⋅))))) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[e:E].
    X+Y(e)  =  if  e  \mmember{}\msubb{}  X  then  inl  X(e)  else  inr  Y(e)    fi    supposing  \muparrow{}e  \mmember{}\msubb{}  X+Y


By

---

Latex:
(Auto
  THEN  Auto
  THEN  (MoveToConcl  (-1)  THEN  All  (Unfold  `eclass`))
  THEN  RepUR  ``es-interface-union  eclass-compose2  in-eclass  eclass-val``  0
  THEN  RepeatFor  2  ((AutoSplit
                                        THEN  Try  ((Auto  THEN  (BLemma  `single-valued-bag-if-le1`  THEN  Auto)\mcdot{}))
                                        )))

---

Home Index