---

Step * 2 of Lemma bag-filter-equal


1. T : Type
2. p1 : T ⟶ 𝔹
3. p2 : T ⟶ 𝔹
4. b : bag(T)
5. ∀x:T. (x ↓∈ b ⇒ (↑p1[x] ⇐⇒ ↑p2[x]))
⊢ [x∈b|p1[x]] = [x∈b|p2[x]] ∈ bag(T)
BY
{ ((BagToList (-2) THENA (Auto THEN DoSubsume THEN Auto))
   THEN RepUR ``bag-filter`` 0
   THEN (InstLemma `filter-sq` [⌜T⌝;⌜b⌝;⌜λx.p1[x]⌝;⌜λx.p2[x]⌝]⋅
         THENA (Auto
                THEN All (RepUR ``so_apply``)
                THEN D (-2)
                THEN (Unhide THENA Auto)
                THEN (InstHyp [⌜x⌝] (-4)⋅ THENA (Auto THEN BLemma `list-member-bag-member` THEN Auto))
                THEN BHyp (-1) 
                THEN Auto)
         )
   THEN HypSubst' (-1) 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  p1  :  T  {}\mrightarrow{}  \mBbbB{}
3.  p2  :  T  {}\mrightarrow{}  \mBbbB{}
4.  b  :  bag(T)
5.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\muparrow{}p1[x]  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}p2[x]))
\mvdash{}  [x\mmember{}b|p1[x]]  =  [x\mmember{}b|p2[x]]


By

---

Latex:
((BagToList  (-2)  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
  THEN  RepUR  ``bag-filter``  0
  THEN  (InstLemma  `filter-sq`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}\mlambda{}x.p1[x]\mkleeneclose{};\mkleeneopen{}\mlambda{}x.p2[x]\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  All  (RepUR  ``so\_apply``)
                            THEN  D  (-2)
                            THEN  (Unhide  THENA  Auto)
                            THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THENA  (Auto  THEN  BLemma  `list-member-bag-member`  THEN  Auto))
                            THEN  BHyp  (-1) 
                            THEN  Auto)
              )
  THEN  HypSubst'  (-1)  0
  THEN  Auto)

---

Home Index