---

Step * of Lemma compose-fpf_wf

∀[A:Type]. ∀[B:A ─→ Type]. ∀[f:x:A fp-> B[x]]. ∀[C:Type]. ∀[a:A ─→ (C?)]. ∀[b:C ─→ A].
  compose-fpf(a;b;f) ∈ y:C fp-> B[b y] supposing ∀y:A. ((↑isl(a y)) ⇒ ((b outl(a y)) = y ∈ A))
BY
{ (Auto
   THEN Unfolds ``fpf compose-fpf`` 0
   THEN (Auto THEN Try ((Reduce (-1) THEN D -1 THEN Unhide THEN Auto)))
   THEN DVar `f'
   THEN Unfolds ``compose fpf-domain`` 0
   THEN Reduce 0
   THEN MemCD
   THEN Reduce 0
   THEN Auto
   THEN All Reduce
   THEN Try (((D (-1)) THEN Unhide THEN Auto))
   THEN Auto
   THEN Try (((RWO "member_map_filter" (-1)) THENA Auto))
   THEN All Reduce
   THEN Try (((D (-1)) THEN Unhide THEN Auto))
   THEN Auto
   THEN ExRepD
   THEN MemTypeCD
   THEN Auto
   THEN (HypSubst (-1) 0)
   THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:x:A  fp->  B[x]].  \mforall{}[C:Type].  \mforall{}[a:A  {}\mrightarrow{}  (C?)].  \mforall{}[b:C  {}\mrightarrow{}  A].
    compose-fpf(a;b;f)  \mmember{}  y:C  fp->  B[b  y]  supposing  \mforall{}y:A.  ((\muparrow{}isl(a  y))  {}\mRightarrow{}  ((b  outl(a  y))  =  y))


By

(Auto
  THEN  Unfolds  ``fpf  compose-fpf``  0
  THEN  (Auto  THEN  Try  ((Reduce  (-1)  THEN  D  -1  THEN  Unhide  THEN  Auto)))
  THEN  DVar  `f'
  THEN  Unfolds  ``compose  fpf-domain``  0
  THEN  Reduce  0
  THEN  MemCD
  THEN  Reduce  0
  THEN  Auto
  THEN  All  Reduce
  THEN  Try  (((D  (-1))  THEN  Unhide  THEN  Auto))
  THEN  Auto
  THEN  Try  (((RWO  "member\_map\_filter"  (-1))  THENA  Auto))
  THEN  All  Reduce
  THEN  Try  (((D  (-1))  THEN  Unhide  THEN  Auto))
  THEN  Auto
  THEN  ExRepD
  THEN  MemTypeCD
  THEN  Auto
  THEN  (HypSubst  (-1)  0)
  THEN  Auto)

---

Home Index