---

Step * of Lemma no_repeats_filter2

∀[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)}  ⟶ 𝔹].  no_repeats(T;filter(P;l)) supposing no_repeats(T;l)
BY
{ RepeatFor 4 ((D 0 THEN Try ((Complete (Auto) ORELSE (DoSubsume THEN Auto))))) }

1
1. T : Type
2. l : T List
3. P : {x:T| (x ∈ l)}  ⟶ 𝔹
4. no_repeats(T;l)
⊢ no_repeats(T;filter(P;l))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[l:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  l)\}    {}\mrightarrow{}  \mBbbB{}].
    no\_repeats(T;filter(P;l))  supposing  no\_repeats(T;l)


By

---

Latex:
RepeatFor  4  ((D  0  THEN  Try  ((Complete  (Auto)  ORELSE  (DoSubsume  THEN  Auto)))))

---

Home Index