---

Step * 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. L = b ∈ pertype(λas,bs. ((as ∈ A List) ∧ (bs ∈ A List) ∧ permutation(A;as;bs)))
7. L ∈ A List
8. b ∈ A List
9. permutation(A;L;b)
10. (x ∈ L)
⊢ ↓∃L:{x:A| P[x]}  List. ((L = b ∈ bag({x:A| P[x]} )) ∧ (x ∈ L))
BY
{ RepeatFor 3 (Thin (-3)) }

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)
⊢ ↓∃L:{x:A| P[x]}  List. ((L = b ∈ bag({x:A| P[x]} )) ∧ (x ∈ L))

---

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.  L  =  b
7.  L  \mmember{}  A  List
8.  b  \mmember{}  A  List
9.  permutation(A;L;b)
10.  (x  \mmember{}  L)
\mvdash{}  \mdownarrow{}\mexists{}L:\{x:A|  P[x]\}    List.  ((L  =  b)  \mwedge{}  (x  \mmember{}  L))


By

---

Latex:
RepeatFor  3  (Thin  (-3))

---

Home Index