(6steps total)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
absval
elim
1
1.
P
:
Prop
(
x
:
.
P
(|
x
|))
(
x
:
.
P
(
x
))
By:
Auto
Generated subgoals:
1
2.
x
:
.
P
(|
x
|)
3.
x
:
P
(
x
)
2
steps
2
2.
x
:
.
P
(
x
)
3.
x
:
P
(|
x
|)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
Prop
(
x:. P(|x|)) 
(x:
. P(x))Prop
(x:. P(|x|)) (x:. P(x))x:. P(|x|)
P(x)
x:. P(x)
P(|x|)
