---

Step * 2 of Lemma decidable__exists-single-valued-bag


1. T : Type
2. b : bag(T)@i
3. single-valued-bag(b;T)@i
4. ∃v:T. v ↓∈ b@i
⊢ 0 < #(b)
BY
{ (D (-1) THEN FLemma `bag-member-size` [-1] THEN Auto) }

---

Latex:



1.  T  :  Type
2.  b  :  bag(T)@i
3.  single-valued-bag(b;T)@i
4.  \mexists{}v:T.  v  \mdownarrow{}\mmember{}  b@i
\mvdash{}  0  <  \#(b)


By

(D  (-1)  THEN  FLemma  `bag-member-size`  [-1]  THEN  Auto)

---

Home Index