Nuprl Lemma : TR4a
[T:Type]. 
[P:T 
 
]. 
[C:
].
  ((C 
 (
C)) 
 (
x:T. True) 
 ((
(
x:T. (P x))) 
 (
x:T. (
(P x)))) 
 ((
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], 
not:
A, 
implies: P 
 Q, 
or: P 
 Q, 
true: True, 
apply: f a, 
function: x:A 
 B[x], 
universe: Type
Definitions : 
implies: P 
 Q, 
member: t 
 T, 
prop:
, 
so_lambda: 
x.t[x], 
all:
x:A. B[x], 
exists:
x:A. B[x], 
subtype_rel: A 
r B, 
not:
A, 
uall:
[x:A]. B[x], 
so_apply: x[s], 
or: P 
 Q, 
false: False
Lemmas : 
all_wf, 
not_wf, 
exists_wf, 
true_wf, 
or_wf
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[C:\mBbbP{}].
    ((C  \mvee{}  (\mneg{}C))
    {}\mRightarrow{}  (\mexists{}x:T.  True)
    {}\mRightarrow{}  ((\mneg{}(\mforall{}x:T.  (P  x)))  {}\mRightarrow{}  (\mexists{}x:T.  (\mneg{}(P  x))))
    {}\mRightarrow{}  ((\mforall{}x:T.  (P  x))  {}\mRightarrow{}  C)
    {}\mRightarrow{}  (\mexists{}x:T.  ((P  x)  {}\mRightarrow{}  C)))
Date html generated:
2014_07_17-AM-09_55_38
Last ObjectModification:
2014_06_18-PM-01_42_02
Home
Index