---

Step * of Lemma bag-filter-no-repeats2

∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  bag-no-repeats({x:T| ↑p[x]} ;[x∈bs|p[x]]) supposing bag-no-repeats(T;bs)
BY
{ (InstLemma `bag-filter-no-repeats` []
   THEN RepeatFor 4 (ParallelLast')
   THEN InstLemma `bag-no-repeats-subtype` [⌜T⌝;⌜{x:T| ↑p[x]} ⌝;⌜[x∈bs|p[x]]⌝]⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `bag-filter-no-repeats`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  InstLemma  `bag-no-repeats-subtype`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\{x:T|  \muparrow{}p[x]\}  \mkleeneclose{};\mkleeneopen{}[x\mmember{}bs|p[x]]\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index