---

Step * of Lemma decidable__exists-single-valued-bag

∀[T:Type]. ∀b:bag(T). (single-valued-bag(b;T) ⇒ Dec(∃v:T. v ↓∈ b))
BY
{ ((UnivCD THENA Auto) THEN (Assert Dec(0 < #(b)) BY Auto) THEN Repeat (ParallelLast)) }

1
1. [T] : Type
2. b : bag(T)@i
3. single-valued-bag(b;T)@i
4. 0 < #(b)
⊢ ∃v:T. v ↓∈ b

2
1. T : Type
2. b : bag(T)@i
3. single-valued-bag(b;T)@i
4. ∃v:T. v ↓∈ b@i
⊢ 0 < #(b)

---

Latex:


\mforall{}[T:Type].  \mforall{}b:bag(T).  (single-valued-bag(b;T)  {}\mRightarrow{}  Dec(\mexists{}v:T.  v  \mdownarrow{}\mmember{}  b))


By

((UnivCD  THENA  Auto)  THEN  (Assert  Dec(0  <  \#(b))  BY  Auto)  THEN  Repeat  (ParallelLast))

---

Home Index