num
thy
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
6
Thm*
a
,
b
:
. (
a
~
b
)
a
=
b
[assoced_nelim]
cites the following:
5
Thm*
a
,
b
:
. (
a
~
b
)
a
=
b
a
= -
b
[assoced_elim]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
num
thy
1
Sections
StandardLIB
Doc
a,b:
. (a ~ b) 
a = ba,b:
. (a ~ b) a = b 
a = -ba,b:. (a ~ b) a = ba,b:. (a ~ b) a = b a = -b