IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
assoced elim1 1. a : 2. b : a | b & b | aa = ba = -b
By:
(RWH (LemmaC Thm*a,b:. a | b & b | aa = b) 0)
THEN
(Unfold `pm_equal` 0)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
a | b & b | a 
a = b 
a = -b
a,b:
b) 0)
