---

Step * 1 of Lemma bag-bind-empty-right


1. A : Type
2. ba : bag(A)
3. L : Top List
4. ba = L ∈ (Top List)
⊢ bag-bind(L;λa.{}) ~ {}
BY
{ (RepUR ``bag-bind empty-bag bag-map bag-union concat`` 0⋅ THEN All Thin THEN ListInd (-1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  ba  :  bag(A)
3.  L  :  Top  List
4.  ba  =  L
\mvdash{}  bag-bind(L;\mlambda{}a.\{\})  \msim{}  \{\}


By

---

Latex:
(RepUR  ``bag-bind  empty-bag  bag-map  bag-union  concat``  0\mcdot{}
  THEN  All  Thin
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index