1. a : 
2. b : 
3. b | a
4. b | 0
5. z:. z | a & z | 0  z | b
6. a | b
  a = b  a = -b

By:	Fold `pm_equal` 0 THEN BackThru Thm* a,b:. a | b  b | a  a =  b

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html