(8steps) PrintForm Definitions int 2 Sections StandardLIB Doc

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

P(x)
By:
MoveToConcl 3
THEN
Unfold `absval` 0
Generated subgoal:

1 P(if 0x x else -x fi) P(x)

About:
ifthenelseintnatural_numberminusapplyfunctionpropimplies

(8steps) PrintForm Definitions int 2 Sections StandardLIB Doc