Definitions
well
fnd
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
rev_implies
Def
P
Q
==
Q
P
Thm*
A
,
B
:Prop. (
A
B
)
Prop
wellfounded
Def
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
Def
==
P
:(
A
Prop). (
j
:
A
. (
k
:
A
.
R
(
k
;
j
)
P
(
k
))
P
(
j
))
{
n
:
A
.
P
(
n
)}
Thm*
A
:Type{i},
r
:(
A
A
Prop{i}). WellFnd{i}(
A
;
x
,
y
.
r
(
x
,
y
))
Prop{i'}
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Definitions
well
fnd
Sections
StandardLIB
Doc