---

Step * of Lemma bag-remove-repeats-filter

∀[T:Type]. ∀[b:bag(T)]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹].
  (bag-remove-repeats(eq;[x∈b|P[x]]) = [x∈bag-remove-repeats(eq;b)|P[x]] ∈ bag(T))
BY
{ ((UnivCD THENA Auto)
   THEN (BagToList 2 THENA Auto)
   THEN RepUR ``bag-remove-repeats bag-filter`` 0
   THEN RWO "list-to-set-filter" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[eq:EqDecider(T)].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
    (bag-remove-repeats(eq;[x\mmember{}b|P[x]])  =  [x\mmember{}bag-remove-repeats(eq;b)|P[x]])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (BagToList  2  THENA  Auto)
  THEN  RepUR  ``bag-remove-repeats  bag-filter``  0
  THEN  RWO  "list-to-set-filter"  0
  THEN  Auto)

---

Home Index