---

Step * of Lemma es-interface-right-as-image

∀[Info,A,B:Type]. ∀[X:EClass(A + B)].  (right(X) = λx.case x of inl(a) => {} | inr(b) => {b}[X] ∈ EClass(B))
BY
{ (Auto
   THEN RepUR ``eclass eclass-compose1 es-interface-right es-filter-image`` 0
   THEN RepeatFor 2 ((EqCD THENA Auto))
   THEN Folds ``in-eclass eclass-val`` 0
   THEN AutoSplit) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A + B)
5. eo : EO+(Info)@i'
6. e : E@i
7. ↑e ∈b X
⊢ (snd(bag-separate(X eo e))) = case X(e) of inl(a) => {} | inr(b) => {b} ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A  +  B)].    (right(X)  =  \mlambda{}x.case  x  of  inl(a)  =>  \{\}  |  inr(b)  =>  \{b\}[X])


By

---

Latex:
(Auto
  THEN  RepUR  ``eclass  eclass-compose1  es-interface-right  es-filter-image``  0
  THEN  RepeatFor  2  ((EqCD  THENA  Auto))
  THEN  Folds  ``in-eclass  eclass-val``  0
  THEN  AutoSplit)

---

Home Index