---

Step * 1 of Lemma non-empty-bag-union-of-list


1. [T] : Type
⊢ 0 < #(bag-union([])) ⇐⇒ (∃b∈[]. 0 < #(b))
BY
{ (RepUR ``bag-union bag-size`` 0 THEN RWO "l_exists_nil" 0 THEN Auto THEN D -1 THEN AutoSimpHyp Auto (-1)) }

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  0  <  \#(bag-union([]))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}[].  0  <  \#(b))


By

---

Latex:
(RepUR  ``bag-union  bag-size``  0
  THEN  RWO  "l\_exists\_nil"  0
  THEN  Auto
  THEN  D  -1
  THEN  AutoSimpHyp  Auto  (-1))

---

Home Index