---

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


1. [T] : Type
2. b : bag(T)@i
3. single-valued-bag(b;T)@i
4. 0 < #(b)
⊢ ∃v:T. v ↓∈ b
BY
{ (InstConcl [⌈sv-bag-only(b)⌉]⋅ THEN Auto THEN BLemma `bag-member-sv-bag-only` THEN Auto) }

---

Latex:



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


By

(InstConcl  [\mkleeneopen{}sv-bag-only(b)\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  BLemma  `bag-member-sv-bag-only`  THEN  Auto)

---

Home Index