---

Step * 1 1 of Lemma sv-bag-tail-single-valued


1. A : Type
2. bs : bag(A)
3. single-valued-bag(bs;A)@i
4. 0 < ||bs||@i
5. single-valued-list(bs;A)
6. bs ∈ A List
7. single-valued-list(tl(bs);A)
⊢ single-valued-bag(tl(bs);A)
BY
{ (BLemma `single-valued-list-sv-bag` THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  bs  :  bag(A)
3.  single-valued-bag(bs;A)@i
4.  0  <  ||bs||@i
5.  single-valued-list(bs;A)
6.  bs  \mmember{}  A  List
7.  single-valued-list(tl(bs);A)
\mvdash{}  single-valued-bag(tl(bs);A)


By

---

Latex:
(BLemma  `single-valued-list-sv-bag`  THEN  Auto)

---

Home Index