---

Step * 1 1 of Lemma bag-member-sv-bag-only


1. T : Type
2. b : bag(T)
3. single-valued-bag(b;T)
4. 0 < #(b)
⊢ mklist(#(b);λx.sv-bag-only(b)) = b ∈ bag(T)
BY
{ ((InstLemma `bag_to_squash_list` [⌜T⌝;⌜b⌝]⋅ THENA Auto)
   THEN TrySquashExRepD (-1)
   THEN MoveToConcl (-4)
   THEN MoveToConcl (-3)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN RepUR ``bag-size sv-bag-only single-valued-bag`` 0
   THEN Auto
   THEN ThinVar `b'
   THEN (EqTypeCD THENA Auto)) }

1
.....antecedent..... 
1. T : Type
2. L : T List
3. 0 < ||L||
4. ∀x,y:T.  (x ↓∈ L ⇒ y ↓∈ L ⇒ (x = y ∈ T))
⊢ permutation(T;mklist(||L||;λx.hd(L));L)

---

Latex:

---

Latex:

1.  T  :  Type
2.  b  :  bag(T)
3.  single-valued-bag(b;T)
4.  0  <  \#(b)
\mvdash{}  mklist(\#(b);\mlambda{}x.sv-bag-only(b))  =  b


By

---

Latex:
((InstLemma  `bag\_to\_squash\_list`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  TrySquashExRepD  (-1)
  THEN  MoveToConcl  (-4)
  THEN  MoveToConcl  (-3)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  RepUR  ``bag-size  sv-bag-only  single-valued-bag``  0
  THEN  Auto
  THEN  ThinVar  `b'
  THEN  (EqTypeCD  THENA  Auto))

---

Home Index