---

Step * of Lemma single-valued-bag-if-le1

∀[T:Type]. ∀[b:bag(T)].  single-valued-bag(b;T) supposing #(b) ≤ 1
BY
{ ((UnivCD THENA Auto)
   THEN (Unfold `single-valued-bag` 0 THEN Auto)
   THEN (Assert ⌜(#(b) = 0 ∈ ℤ) ∨ (#(b) = 1 ∈ ℤ)⌝⋅ THENA Auto')
   THEN Thin 3
   THEN (BagToList 2 THENA Auto)
   THEN Unfold `bag-size` (-1)
   THEN D (-1)) }

1
1. T : Type
2. b : T List
3. x : T
4. y : T
5. x ↓∈ b
6. y ↓∈ b
7. ||b|| = 0 ∈ ℤ
⊢ x = y ∈ T

2
1. T : Type
2. b : T List
3. x : T
4. y : T
5. x ↓∈ b
6. y ↓∈ b
7. ||b|| = 1 ∈ ℤ
⊢ x = y ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].    single-valued-bag(b;T)  supposing  \#(b)  \mleq{}  1


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Unfold  `single-valued-bag`  0  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}(\#(b)  =  0)  \mvee{}  (\#(b)  =  1)\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  Thin  3
  THEN  (BagToList  2  THENA  Auto)
  THEN  Unfold  `bag-size`  (-1)
  THEN  D  (-1))

---

Home Index