---

{ [A:Type]. [eq:EqDecider(A)]. [B:A  Type]. [f:x:A fp-> B[x]].
  [P:x:{x:A| x  dom(f)}   B[x]  ].
    (xdom(f). v=f(x)   P[x;v]  ) }

{ Proof }

---

Definitions occuring in Statement :  fpf-all: xdom(f). v=f(x)   P[x; v],  fpf-dom: x  dom(f),  fpf: a:A fp-> B[a],  assert: b,  uall: [x:A]. B[x],  prop: ,  so_apply: x[s1;s2],  so_apply: x[s],  member: t  T,  set: {x:A| B[x]} ,  function: x:A  B[x],  universe: Type,  deq: EqDecider(T)
Definitions :  uall: [x:A]. B[x],  so_apply: x[s],  prop: ,  member: t  T,  fpf-all: xdom(f). v=f(x)   P[x; v],  so_apply: x[s1;s2],  all: x:A. B[x],  implies: P  Q,  so_lambda: x.t[x],  uimplies: b supposing a
Lemmas :  assert_wf,  fpf-dom_wf,  fpf-trivial-subtype-top,  fpf-ap_wf,  fpf_wf,  deq_wf

---

\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:x:A  fp->  B[x]].  \mforall{}[P:x:\{x:A|  \muparrow{}x  \mmember{}  dom(f)\} 
                                                                                                                                              {}\mrightarrow{}  B[x]
                                                                                                                                              {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}x\mmember{}dom(f).  v=f(x)  {}\mRightarrow{}    P[x;v]  \mmember{}  \mBbbP{})


Date html generated: 2011_08_10-AM-08_03_59
Last ObjectModification: 2011_06_18-AM-08_22_22

Home Index