---

Step * 2 of Lemma assert-bag-null


1. T : Type
2. bs : bag(T)
3. bs = {} ∈ bag(T)
⊢ ↑bag-null(bs)
BY
{ ((HypSubst (-1) 0 THEN Auto) THEN RepUR ``bag-null empty-bag`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  bag(T)
3.  bs  =  \{\}
\mvdash{}  \muparrow{}bag-null(bs)


By

---

Latex:
((HypSubst  (-1)  0  THEN  Auto)  THEN  RepUR  ``bag-null  empty-bag``  0  THEN  Auto)

---

Home Index