Nuprl Lemma : TR8b
[T:Type]. 
[P:T ![](../FONT/dash.png)
 
]. 
[C:
].  ((
x:T. True) ![](../FONT/eq.png)
 (
x:T. ((P x) 
 C)) ![](../FONT/eq.png)
 ((
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 ![](../FONT/eq.png)
 Q, 
and: P 
 Q, 
true: True, 
apply: f a, 
function: x:A ![](../FONT/dash.png)
 B[x], 
universe: Type
Definitions : 
uall:
[x:A]. B[x], 
member: t 
 T, 
prop:
, 
implies: P ![](../FONT/eq.png)
 Q, 
so_lambda: ![](../FONT/lam.png)
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