(19steps total)
PrintForm
Definitions
int
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nat
ind
tp
1
1
1
1.
P
:
Prop
2.
P
(0)
3.
i
:
.
P
(
i
-1)
P
(
i
)
4.
i
:
5.
i
0
P
(
i
)
By:
p.IntInd (get_int_arg `hn` p) p
Generated subgoals:
1
5.
i
<0
6.
i
+1
0
P
(
i
+1)
i
0
P
(
i
)
3
steps
2
0
0
P
(0)
4
steps
3
5. 0<
i
6.
i
-1
0
P
(
i
-1)
i
0
P
(
i
)
8
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(19steps total)
PrintForm
Definitions
int
1
Sections
StandardLIB
Doc