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

By:	(Rewrite (RevLemmaC Thm* a,b:. |a| | |b|  a | b) 3) THEN (Rewrite (RevLemmaC Thm* a,b:. |a| | |b|  a | b) 4)

1

3. |a| | |b| 4. |b| | |a|   a =  b

4 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html