(6steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: divides anti sym 1 1 1 1
1. a : 
2. b : 
3. |a| | |b|
4. |b| | |a|
5. a,b:. a | b  b | a  a = b
  |a| = |b|
By: Rewrite (SweepUpC (RevLemmaC Thm* P:(Prop). (x:. P(|x|))  (x:. P(x))))
5

Generated subgoal:

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

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

(6steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc