(8steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
At:
absval
elim
2
1.
P:
Prop
2.
x:
. P(x)
3.
x:
P(|x|)
By:
Unfold `absval` 0
Generated subgoal:
1
P(if 0
x
x else -x fi)
About:
(8steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
P(if 0
x
x else -x fi)
Prop
x:
. P(x) P(|x|) P(if 0x x else -x fi)
