1. a : 
2. b : 
3. |a| | |b|
4. |b| | |a|
  |a| = |b|

By:	AssertLemma Thm* a,b:. a | b  b | a  a = b []

1

5. a,b:. a | b  b | a  a = b   |a| = |b|

2 steps

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