---

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

.....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)
BY
{ ((BLemma `permutation_weakening` THENA Auto)
   THEN (BLemma `list_extensionality` THEN Auto)
   THEN Try (Complete ((RWO "mklist_length" 0 THEN Auto)))
   THEN Auto
   THEN (RWO "mklist_length" (-1) THENA Auto)
   THEN (InstLemma `mklist_select` [⌜T⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "select0<" 0 THENA Auto)
   THEN (BHyp (-4)  THENA Auto)
   THEN Unfold `bag-member` 0
   THEN D 0
   THEN InstConcl [⌜L⌝]⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  L  :  T  List
3.  0  <  ||L||
4.  \mforall{}x,y:T.    (x  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  y  \mdownarrow{}\mmember{}  L  {}\mRightarrow{}  (x  =  y))
\mvdash{}  permutation(T;mklist(||L||;\mlambda{}x.hd(L));L)


By

---

Latex:
((BLemma  `permutation\_weakening`  THENA  Auto)
  THEN  (BLemma  `list\_extensionality`  THEN  Auto)
  THEN  Try  (Complete  ((RWO  "mklist\_length"  0  THEN  Auto)))
  THEN  Auto
  THEN  (RWO  "mklist\_length"  (-1)  THENA  Auto)
  THEN  (InstLemma  `mklist\_select`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "select0<"  0  THENA  Auto)
  THEN  (BHyp  (-4)    THENA  Auto)
  THEN  Unfold  `bag-member`  0
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index