---

{ [A:Type]. [B:A  Type].
    f:x:A fp-> B[x]
      [C:Type]
        a:A  (C?). b:C  A. y:C.
          ((y  fpf-domain(compose-fpf(a;b;f)))
           x:A. ((x  fpf-domain(f))  ((isl(a x)) c (y = outl(a x))))) }

{ Proof }

---

Definitions occuring in Statement :  compose-fpf: compose-fpf(a;b;f),  fpf-domain: fpf-domain(f),  fpf: a:A fp-> B[a],  outl: outl(x),  isl: isl(x),  assert: b,  uall: [x:A]. B[x],  cand: A c B,  so_apply: x[s],  all: x:A. B[x],  exists: x:A. B[x],  iff: P  Q,  and: P  Q,  unit: Unit,  apply: f a,  function: x:A  B[x],  union: left + right,  universe: Type,  equal: s = t,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  so_apply: x[s],  member: t  T,  so_lambda: x.t[x],  fpf-domain: fpf-domain(f),  compose-fpf: compose-fpf(a;b;f),  pi1: fst(t),  prop: ,  assert: b,  btrue: tt,  implies: P  Q,  ifthenelse: if b then t else f fi ,  true: True,  exists: x:A. B[x],  and: P  Q,  cand: A c B,  iff: P  Q,  rev_implies: P  Q,  fpf: a:A fp-> B[a],  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T}
Lemmas :  unit_wf,  fpf_wf,  l_member_wf,  mapfilter_wf,  isl_wf,  outl_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert_wf,  assert_elim,  iff_functionality_wrt_iff,  member_map_filter

---

\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.  \mforall{}y:C.
                ((y  \mmember{}  fpf-domain(compose-fpf(a;b;f)))
                \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:A.  ((x  \mmember{}  fpf-domain(f))  \mwedge{}  ((\muparrow{}isl(a  x))  c\mwedge{}  (y  =  outl(a  x)))))


Date html generated: 2011_08_10-AM-08_05_12
Last ObjectModification: 2011_06_18-AM-08_23_04

Home Index