---

Step * of Lemma fpf-map_wf

∀[A,C:Type]. ∀[B:A ─→ Type]. ∀[x:a:A fp-> B[a]]. ∀[f:a:{a:A| (a ∈ fpf-domain(x))}  ─→ B[a] ─→ C].
  (fpf-map(a,v.f[a;v];x) ∈ C List)
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀A,C:Type. ∀B:A ─→ Type. ∀x:a:A fp-> B[a]. ∀f:a:{a:A| (a ∈ fpf-domain(x))}  ─→ B[a] ─→ C.
  (fpf-map(a,v.f[a;v];x) ∈ C List)

---

Latex:


\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[x:a:A  fp->  B[a]].  \mforall{}[f:a:\{a:A|  (a  \mmember{}  fpf-domain(x))\}    {}\mrightarrow{}  B[a]  {}\mrightarrow{}  C].
    (fpf-map(a,v.f[a;v];x)  \mmember{}  C  List)


By

(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index