---

Step * of Lemma bag-no-repeats-filter

∀[T:Type]. ∀[b:bag(T)]. ∀[p:T ⟶ 𝔹].  bag-no-repeats(T;[x∈b|p[x]]) supposing bag-no-repeats(T;b)
BY
{ (Auto
   THEN SquashConcl
   THEN (BagToList (-3) THENA Auto)
   THEN Unfold `bag-filter` 0
   THEN (All(RWO "bag-no-repeats-list") THENA Auto)
   THEN D 0
   THEN BLemma `no_repeats_filter`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].    bag-no-repeats(T;[x\mmember{}b|p[x]])  supposing  bag-no-repeats(T;b)


By

---

Latex:
(Auto
  THEN  SquashConcl
  THEN  (BagToList  (-3)  THENA  Auto)
  THEN  Unfold  `bag-filter`  0
  THEN  (All(RWO  "bag-no-repeats-list")  THENA  Auto)
  THEN  D  0
  THEN  BLemma  `no\_repeats\_filter`
  THEN  Auto)

---

Home Index