---

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
{ (UnivCD THENA Auto) }

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:


\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

(UnivCD  THENA  Auto)

---

Home Index