---

Step * 1 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
{ (((Unfold `fpf-domain` 0
     THEN Repeat ((D 0 THENA Complete (Auto)))
     THEN DVar `x'
     THEN Unfold `fpf-map` 0
     THEN Reduce 0)
    THENA Auto
    )
   THEN BLemma `map-wf2`
   THEN Try (Complete (Auto)))⋅ }

---

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

(((Unfold  `fpf-domain`  0
      THEN  Repeat  ((D  0  THENA  Complete  (Auto)))
      THEN  DVar  `x'
      THEN  Unfold  `fpf-map`  0
      THEN  Reduce  0)
    THENA  Auto
    )
  THEN  BLemma  `map-wf2`
  THEN  Try  (Complete  (Auto)))\mcdot{}

---

Home Index