(4steps total) PrintForm num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: divides transitivity 1
1. a : 
2. b : 
3. c : 
4. c:. b = ac
5. c@0:. c = bc@0
  c@0:. c = ac@0
By: Analyze 5 THEN Analyze 4

Generated subgoal:

1 4. c1 : 
5. b = ac1
6. c@0 : 
7. c = bc@0
  c@0:. c = ac@0
2 steps

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

(4steps total) PrintForm num thy 1 Sections StandardLIB Doc