---

Step * 1 2 of Lemma bag-filter-equal


1. T : Type
2. p1 : T ⟶ 𝔹
3. p2 : T ⟶ 𝔹
4. b : bag(T)
5. [x∈b|p1[x]] = [x∈b|p2[x]] ∈ bag(T)
6. x : T
7. x ↓∈ b
8. ↑p2[x]
⊢ ↑p1[x]
BY
{ ((InstLemma `bag-member-filter` [⌜T⌝;⌜p2⌝;⌜x⌝;⌜b⌝]⋅ THENA Auto)
   THEN D (-1)
   THEN Thin (-2)
   THEN (D (-1) THENA Auto)
   THEN (RevHypSubst' (-5) (-1) THENA Auto)
   THEN BagMemberD (-1)
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `bag-member-filter`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Thin  (-2)
  THEN  (D  (-1)  THENA  Auto)
  THEN  (RevHypSubst'  (-5)  (-1)  THENA  Auto)
  THEN  BagMemberD  (-1)
  THEN  Auto)

---

Home Index