(6steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
divides
anti
sym
1
1
1.
a
:
2.
b
:
3. |
a
| | |
b
|
4. |
b
| | |
a
|
a
=
b
By:
Rewrite (RevLemmaC
Thm*
x
,
y
:
. |
x
| = |
y
|
x
=
y
) 0
Generated subgoal:
1
|
a
| = |
b
|
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
a = 
b
a = b
x,y:. |x| = |y| 
x = y) 0 |a| = |b|
