(8steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
At:
absval
elim
1
1.
P:
Prop
2.
x:
. P(|x|)
3.
x:
P(x)
By:
DTerm x 2
Generated subgoal:
1
2.
x:
3.
P(|x|)
P(x)
About:
(8steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
P(x)
Prop
x:. P(|x|) P(x) P(x)
