NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
(
n
.
n
<
0) = (
n
.false
)
[sfa_doc_sqtype_ctr_example_part2]
cites the following:
1
Thm*
b
:
.
b
b
= false
[not_assert_elim]
1
Thm*
x
,
y
:
.
x
<
y
x
<
y
[assert_of_lt_int]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NuprlPrimitives
Sections
NuprlLIB
Doc
n.n<
0) = (n.false) 
b:. 
b 
b = falsex,y:
. x<y 
x<yn.n<0) = (n.false) b:. b b = falsex,y:. x<y x<y