---

Step * 1 2 2 1 of Lemma empty-bag-union

.....antecedent..... 
1. T : Type
2. bs : bag(bag(T))
3. bag-union(bs) = {} ∈ bag(T)
⊢ concat(bs) = [] ∈ (Top List)
BY
{ ((Unfolds ``bag-union empty-bag`` (-1) THEN HypSubst' -1 0) THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  bs  :  bag(bag(T))
3.  bag-union(bs)  =  \{\}
\mvdash{}  concat(bs)  =  []


By

---

Latex:
((Unfolds  ``bag-union  empty-bag``  (-1)  THEN  HypSubst'  -1  0)  THEN  Auto)

---

Home Index