---

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


1. A : Type
2. bs : bag(A)
3. single-valued-bag(bs;A)
⊢ single-valued-list(bs;A)
BY
{ (Unfold `single-valued-list` 0
   THEN Auto
   THEN Try ((BLemma `single-valued-bag-is-list` THEN Auto))
   THEN Unfold `single-valued-bag` 3
   THEN BackThruSomeHyp) }

1
1. A : Type
2. bs : bag(A)
3. ∀x,y:A.  (x ↓∈ bs ⇒ y ↓∈ bs ⇒ (x = y ∈ A))
4. x : A@i
5. y : A@i
6. (x ∈ bs)@i
7. (y ∈ bs)@i
⊢ x ↓∈ bs

2
1. A : Type
2. bs : bag(A)
3. ∀x,y:A.  (x ↓∈ bs ⇒ y ↓∈ bs ⇒ (x = y ∈ A))
4. x : A@i
5. y : A@i
6. (x ∈ bs)@i
7. (y ∈ bs)@i
⊢ y ↓∈ bs

---

Latex:

---

Latex:

1.  A  :  Type
2.  bs  :  bag(A)
3.  single-valued-bag(bs;A)
\mvdash{}  single-valued-list(bs;A)


By

---

Latex:
(Unfold  `single-valued-list`  0
  THEN  Auto
  THEN  Try  ((BLemma  `single-valued-bag-is-list`  THEN  Auto))
  THEN  Unfold  `single-valued-bag`  3
  THEN  BackThruSomeHyp)

---

Home Index