---

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

∀[Info,A,B:Type]. ∀[X:EClass(A + B)].  (left(X) = λx.case x of inl(a) => {a} | inr(b) => {}[X] ∈ EClass(A))
BY
{ (Auto
   THEN RepUR ``eclass eclass-compose1 es-interface-left es-filter-image`` 0
   THEN RepeatFor 2 ((EqCD THENA Auto))
   THEN Folds ``in-eclass eclass-val`` 0
   THEN AutoSplit
   THEN (InstLemma `single-eclass-val` [⌜Info⌝;⌜λ2es e.A + B⌝;⌜X⌝;⌜eo⌝;⌜e⌝]⋅ THENA Auto)
   THEN HypSubst (-1) 0
   THEN Auto
   THEN GenConclAtAddr [3;1]
   THEN All Thin) }

1
1. A : Type
2. B : Type
3. v : A + B@i
⊢ (fst(bag-separate({v}))) = case v of inl(a) => {a} | inr(b) => {} ∈ bag(A)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``eclass  eclass-compose1  es-interface-left  es-filter-image``  0
  THEN  RepeatFor  2  ((EqCD  THENA  Auto))
  THEN  Folds  ``in-eclass  eclass-val``  0
  THEN  AutoSplit
  THEN  (InstLemma  `single-eclass-val`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}es  e.A  +  B\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst  (-1)  0
  THEN  Auto
  THEN  GenConclAtAddr  [3;1]
  THEN  All  Thin)

---

Home Index