---

Step * 1 1 1 of Lemma bag-subtype2


1. A : Type
2. P : A ⟶ ℙ
3. b : {x:A| P[x]}  List
4. x : {x:A| P[x]} 
5. L : A List
6. permutation(A;L;b)
7. (x ∈ L)
⊢ ↓∃L:{x:A| P[x]}  List. ((L = b ∈ bag({x:A| P[x]} )) ∧ (x ∈ L))
BY
{ ((Assert ⌜L ∈ {x:A| P[x]}  List⌝⋅
    THENA ((FLemma `permutation_inversion` [-2] THENA Auto)
           THEN Unfold `permutation` (-1)
           THEN ExRepD
           THEN (InstLemma `permute_list_wf` [⌜{x:A| P[x]} ⌝;⌜b⌝;⌜f⌝]⋅ THENA Auto)
           THEN InstLemma `list-eq-subtype2` [⌜A⌝;⌜P⌝;⌜(b o f)⌝;⌜L⌝]⋅
           THEN Auto)
    )
   THEN D 0
   THEN InstConcl [⌜L⌝]⋅
   THEN Auto
   THEN EqTypeCD
   THEN Auto)⋅ }

1
1. A : Type
2. P : A ⟶ ℙ
3. b : {x:A| P[x]}  List
4. x : {x:A| P[x]} 
5. L : A List
6. {permutation(A;L;b)}
7. (x ∈ L)
8. L ∈ {x:A| P[x]}  List
9. permutation(A;L;b)
⊢ ...system_error_message... permutation({x:A| P[x]} ;L;b)

---

Latex:

---

Latex:

1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbP{}
3.  b  :  \{x:A|  P[x]\}    List
4.  x  :  \{x:A|  P[x]\} 
5.  L  :  A  List
6.  permutation(A;L;b)
7.  (x  \mmember{}  L)
\mvdash{}  \mdownarrow{}\mexists{}L:\{x:A|  P[x]\}    List.  ((L  =  b)  \mwedge{}  (x  \mmember{}  L))


By

---

Latex:
((Assert  \mkleeneopen{}L  \mmember{}  \{x:A|  P[x]\}    List\mkleeneclose{}\mcdot{}
    THENA  ((FLemma  `permutation\_inversion`  [-2]  THENA  Auto)
                  THEN  Unfold  `permutation`  (-1)
                  THEN  ExRepD
                  THEN  (InstLemma  `permute\_list\_wf`  [\mkleeneopen{}\{x:A|  P[x]\}  \mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  InstLemma  `list-eq-subtype2`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}(b  o  f)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
                  THEN  Auto)
    )
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  EqTypeCD
  THEN  Auto)\mcdot{}

---

Home Index