---

Step * of Lemma bag-filter-no-repeats

No Annotations
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  bag-no-repeats(T;[x∈bs|p[x]]) supposing bag-no-repeats(T;bs)
BY
{ ((Unfold `bag-no-repeats` 0 THEN Auto)
   THEN BagToList 3
   THEN Auto
   THEN Try ((DoSubsume THEN Auto))
   THEN (SquashExRepD THEN (EqTypeHD (-2) THENA Auto))⋅) }

1
1. T : Type
2. p : T ⟶ 𝔹
3. bs : T List
4. L@0 : T List
5. L@0 = bs ∈ (as,bs:T List//permutation(T;as;bs))
6. L@0 ∈ T List
7. bs ∈ T List
8. permutation(T;L@0;bs)
9. no_repeats(T;L@0)
⊢ ↓∃L@0:T List. ((L@0 = [x∈bs|p[x]] ∈ bag(T)) ∧ no_repeats(T;L@0))

---

Latex:

---

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


By

---

Latex:
((Unfold  `bag-no-repeats`  0  THEN  Auto)
  THEN  BagToList  3
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto))
  THEN  (SquashExRepD  THEN  (EqTypeHD  (-2)  THENA  Auto))\mcdot{})

---

Home Index