---

Step * of Lemma equipollent-filter

∀[A:Type]. ∀P:A ⟶ 𝔹. ∀L:A List.  {x:ℕ||L||| ↑P[L[x]]}  ~ ℕ||filter(P;L)||
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN (BLemma `last_induction` THENA Auto) THEN Reduce 0) }

1
1. [A] : Type
2. P : A ⟶ 𝔹
⊢ {x:ℕ0| ↑P[⊥]}  ~ ℕ0

2
1. [A] : Type
2. P : A ⟶ 𝔹
⊢ ∀ys:A List. ∀y:A.
    ({x:ℕ||ys||| ↑P[ys[x]]}  ~ ℕ||filter(P;ys)|| ⇒ {x:ℕ||ys @ [y]||| ↑P[ys @ [y][x]]}  ~ ℕ||filter(P;ys @ [y])||)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.    \{x:\mBbbN{}||L|||  \muparrow{}P[L[x]]\}    \msim{}  \mBbbN{}||filter(P;L)||


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  (BLemma  `last\_induction`  THENA  Auto)  THEN  Reduce  0)

---

Home Index