---

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


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
BY
{ (Fold `single-valued-bag` 3
   THEN (Unfold `bag-member` 0 THEN D 0)
   THEN InstConcl [⌈bs⌉]⋅
   THEN Auto
   THEN BLemma `single-valued-bag-is-list`
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  bs  :  bag(A)
3.  \mforall{}x,y:A.    (x  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  y  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  (x  =  y))
4.  x  :  A@i
5.  y  :  A@i
6.  (x  \mmember{}  bs)@i
7.  (y  \mmember{}  bs)@i
\mvdash{}  y  \mdownarrow{}\mmember{}  bs


By

---

Latex:
(Fold  `single-valued-bag`  3
  THEN  (Unfold  `bag-member`  0  THEN  D  0)
  THEN  InstConcl  [\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  BLemma  `single-valued-bag-is-list`
  THEN  Auto)\mcdot{}

---

Home Index