(8steps) PrintForm Definitions int 2 Sections StandardLIB Doc

At: absval elim 2 1
1. P: Prop
2. x:. P(x)
3. x:

P(if 0x x else -x fi)
By:
BoolCasesOnCExp (0x)
THEN
AbReduce 0
Generated subgoals:

14. 0x
P(x)
24. x < 0
P(-x)

About:
ifthenelseintnatural_numberminusapplyfunctionpropall

(8steps) PrintForm Definitions int 2 Sections StandardLIB Doc