---

Step * of Lemma filter-fpf-vals

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[B:A ⟶ Type]. ∀[P,Q:A ⟶ 𝔹]. ∀[f:x:A fp-> B[x]].
  (filter(λpL.Q[fst(pL)];fpf-vals(eq;P;f)) ~ fpf-vals(eq;λa.((P a) ∧b (Q a));f))
BY
{ xxx(UnivCD THENA Auto)xxx }

1
1. A : Type
2. eq : EqDecider(A)
3. B : A ⟶ Type
4. P : A ⟶ 𝔹
5. Q : A ⟶ 𝔹
6. f : x:A fp-> B[x]
⊢ filter(λpL.Q[fst(pL)];fpf-vals(eq;P;f)) ~ fpf-vals(eq;λa.((P a) ∧b (Q a));f)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[P,Q:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:x:A  fp->  B[x]].
    (filter(\mlambda{}pL.Q[fst(pL)];fpf-vals(eq;P;f))  \msim{}  fpf-vals(eq;\mlambda{}a.((P  a)  \mwedge{}\msubb{}  (Q  a));f))


By

---

Latex:
xxx(UnivCD  THENA  Auto)xxx

---

Home Index