---

Step * 2 1 1 of Lemma bag-no-repeats-settype


1. T : Type
2. bs : bag(T)
3. ∀x,y:T.  Dec(x = y ∈ T)
4. L : T List
5. L = bs ∈ bag(T)
6. no_repeats(T;L)
⊢ L ∈ {x:T| x ↓∈ bs}  List
BY
{ ((BLemma `list-set-type2` THEN Auto)
   THEN D 0
   THEN Auto
   THEN (SubstFor ⌜bs⌝ 0⋅ THEN Auto)
   THEN BLemma `bag-member-list`
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  bag(T)
3.  \mforall{}x,y:T.    Dec(x  =  y)
4.  L  :  T  List
5.  L  =  bs
6.  no\_repeats(T;L)
\mvdash{}  L  \mmember{}  \{x:T|  x  \mdownarrow{}\mmember{}  bs\}    List


By

---

Latex:
((BLemma  `list-set-type2`  THEN  Auto)
  THEN  D  0
  THEN  Auto
  THEN  (SubstFor  \mkleeneopen{}bs\mkleeneclose{}  0\mcdot{}  THEN  Auto)
  THEN  BLemma  `bag-member-list`
  THEN  Auto)

---

Home Index