---

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
{ xxx(UniformUnivCD Auto THEN Repeat (MoveToConcl (-1)))xxx }

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:

---

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

---

Latex:
xxx(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))xxx

---

Home Index