---

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


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)
BY
{ (D (-1)
   THEN RepUR ``bag-separate single-bag bag-mapfilter bag-map bag-filter`` 0
   THEN Try ((Fold `single-bag` 0 THEN Auto))
   THEN Try ((Fold `empty-bag` 0 THEN Auto)))⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(D  (-1)
  THEN  RepUR  ``bag-separate  single-bag  bag-mapfilter  bag-map  bag-filter``  0
  THEN  Try  ((Fold  `single-bag`  0  THEN  Auto))
  THEN  Try  ((Fold  `empty-bag`  0  THEN  Auto)))\mcdot{}

---

Home Index