---

Step * 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. d1 = d2 ∈ bag(A)
⊢ d1 = d2 ∈ bag({a:A| B[a]} )
BY
{ ((InstLemma `bag_to_squash_list` [⌜{a:A| B[a]} ⌝;⌜d1⌝]⋅ THENA Auto)
   THEN SquashExRepD
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN (Assert ⌜∀A,B:Type. ∀d1,d2:A.  ((A ⊆r B) ⇒ (d1 = d2 ∈ A) ⇒ (d1 = d2 ∈ B))⌝⋅ THENA Auto)
   THEN (InstHyp [⌜bag({a:A| B[a]} )⌝;⌜bag(A)⌝;⌜d1⌝;⌜L⌝] (-1)⋅ THENA Auto)
   THEN (HypSubst' (-1) (-5) THENA Auto)) }

1
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]} )

---

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.  d1  =  d2
\mvdash{}  d1  =  d2


By

---

Latex:
((InstLemma  `bag\_to\_squash\_list`  [\mkleeneopen{}\{a:A|  B[a]\}  \mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SquashExRepD
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mforall{}A,B:Type.  \mforall{}d1,d2:A.    ((A  \msubseteq{}r  B)  {}\mRightarrow{}  (d1  =  d2)  {}\mRightarrow{}  (d1  =  d2))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}bag(\{a:A|  B[a]\}  )\mkleeneclose{};\mkleeneopen{}bag(A)\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-1)  (-5)  THENA  Auto))

---

Home Index