Nuprl Lemma : TR8b
[T:Type]. [P:T  ]. [C:].  ((x:T. True)  (x:T. ((P x)  C))  ((x:T. (P x))  C))
Proof
Definitions occuring in Statement : 
uall: [x:A]. B[x], 
prop: , 
all: x:A. B[x], 
exists: x:A. B[x], 
implies: P  Q, 
and: P  Q, 
true: True, 
apply: f a, 
function: x:A  B[x], 
universe: Type
Definitions : 
uall: [x:A]. B[x], 
member: t  T, 
prop: , 
implies: P  Q, 
so_lambda: x.t[x], 
and: P  Q, 
subtype_rel: A r B, 
all: x:A. B[x], 
so_apply: x[s], 
exists: x:A. B[x]
Lemmas : 
all_wf, 
exists_wf, 
true_wf
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[C:\mBbbP{}].    ((\mexists{}x:T.  True)  {}\mRightarrow{}  (\mforall{}x:T.  ((P  x)  \mwedge{}  C))  {}\mRightarrow{}  ((\mforall{}x:T.  (P  x))  \mwedge{}  C))
Date html generated:
2014_07_17-AM-09_55_54
Last ObjectModification:
2014_06_19-AM-10_57_32
Home
Index