PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
absval
sym
i:
. |i| = |-i|
By:
Analyze 0
THEN
BackThru
Thm*
x,y:
. |x| = |y|
x =
y
THEN
Unfold `pm_equal` 0
Generated subgoals:
None
About:
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
i:
. |i| = |-i|x,y:. |x| = |y| 
x = 
y
