Nuprl Lemma : exists_over_implies_pull

T:Type. P:. Q:T  .  (T  Dec(P)  (P  (x:T. (Q x)))  (x:T. (P  (Q x))))


Proof




Definitions occuring in Statement :  decidable: Dec(P) prop: all: x:A. B[x] exists: x:A. B[x] implies: P  Q apply: f a function: x:A  B[x] universe: Type
Definitions :  all: x:A. B[x] prop: implies: P  Q exists: x:A. B[x] member: t  T so_lambda: x.t[x] uall: [x:A]. B[x] so_apply: x[s] decidable: Dec(P) or: P  Q not: A false: False
Lemmas :  exists_wf decidable_wf
\mforall{}T:Type.  \mforall{}P:\mBbbP{}.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.    (T  {}\mRightarrow{}  Dec(P)  {}\mRightarrow{}  (P  {}\mRightarrow{}  (\mexists{}x:T.  (Q  x)))  {}\mRightarrow{}  (\mexists{}x:T.  (P  {}\mRightarrow{}  (Q  x))))


Date html generated: 2013_03_20-AM-09_45_13
Last ObjectModification: 2013_03_12-PM-06_24_16

Home Index