---

Step * 1 1 of Lemma bag-eq-subtype1


1. A : Type
2. B : A ⟶ ℙ
3. d1 : bag({a:A| B[a]} )
4. d2 : bag({a:A| B[a]} )
5. L : {a:A| B[a]}  List
6. d1 = L ∈ bag({a:A| B[a]} )
7. ∀A,B:Type. ∀d1,d2:A.  ((A ⊆r B) ⇒ (d1 = d2 ∈ A) ⇒ (d1 = d2 ∈ B))
8. d1 = L ∈ bag(A)
9. L = d2 ∈ bag(A)
⊢ L = d2 ∈ bag({a:A| B[a]} )
BY
{ ThinVar `d1' }

1
1. A : Type
2. B : A ⟶ ℙ
3. d2 : bag({a:A| B[a]} )
4. L : {a:A| B[a]}  List
5. ∀A,B:Type. ∀d1,d2:A.  ((A ⊆r B) ⇒ (d1 = d2 ∈ A) ⇒ (d1 = d2 ∈ B))
6. L = d2 ∈ bag(A)
⊢ L = d2 ∈ bag({a:A| B[a]} )

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  \mBbbP{}
3.  d1  :  bag(\{a:A|  B[a]\}  )
4.  d2  :  bag(\{a:A|  B[a]\}  )
5.  L  :  \{a:A|  B[a]\}    List
6.  d1  =  L
7.  \mforall{}A,B:Type.  \mforall{}d1,d2:A.    ((A  \msubseteq{}r  B)  {}\mRightarrow{}  (d1  =  d2)  {}\mRightarrow{}  (d1  =  d2))
8.  d1  =  L
9.  L  =  d2
\mvdash{}  L  =  d2


By

---

Latex:
ThinVar  `d1'

---

Home Index