(4steps 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:
assoced
nelim
a
,
b
:
. (
a
~
b
)
a
=
b
By:
RepD THEN (RWH (LemmaC
Thm*
a
,
b
:
. (
a
~
b
)
a
=
b
a
= -
b
) 0)
Generated subgoal:
1
1.
a
:
2.
b
:
a
=
b
a
= -
b
a
=
b
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
num
thy
1
Sections
StandardLIB
Doc
a,b:
. (a ~ b) 
a = b a,b:. (a ~ b) a = ba,b:
. (a ~ b) a = b 
a = -b) 0)
a = b a = -b a = b
