---

Step * 1 1 1 of Lemma bag-eq-subtype1


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]} )
BY
{ ((InstLemma `bag_to_squash_list` [⌜{a:A| B[a]} ⌝;⌜d2⌝]⋅ THENA Auto)
   THEN SquashExRepD
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN (InstHyp [⌜bag({a:A| B[a]} )⌝;⌜bag(A)⌝;⌜d2⌝;⌜L1⌝] (-4)⋅ THENA Auto)
   THEN (HypSubst' (-1) (-4) THENA Auto)) }

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. L1 : {a:A| B[a]}  List
7. d2 = L1 ∈ bag({a:A| B[a]} )
8. d2 = L1 ∈ bag(A)
9. L = L1 ∈ bag(A)
⊢ L = L1 ∈ bag({a:A| B[a]} )

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `bag\_to\_squash\_list`  [\mkleeneopen{}\{a:A|  B[a]\}  \mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SquashExRepD
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}bag(\{a:A|  B[a]\}  )\mkleeneclose{};\mkleeneopen{}bag(A)\mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-1)  (-4)  THENA  Auto))

---

Home Index