(8steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
At:
absval
elim
P:(
Prop). (
x:
. P(|x|))
(
x:
. P(x))
By:
Unfolds [`guard`;`so_apply`] 0
THEN
GenUnivCD
Generated subgoals:
1
1.
P:
Prop
2.
x:
. P(|x|)
3.
x:
P(x)
2
1.
P:
Prop
2.
x:
. P(x)
3.
x:
P(|x|)
About:
(8steps)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
Prop
x:. P(|x|)
P(x)Propx:. P(x) P(|x|) P:(Prop). (x:. P(|x|)) 
(x:. P(x))Propx:. P(|x|) P(x)Propx:. P(x) P(|x|)
