(5steps 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: eqmod fun
  m,a,a',b,b':.
  (a = a' mod m)  (b = b' mod m)  ((a = b mod m)  (a' = b' mod m))
By: GenUnivCD

Generated subgoals:

1 1. m : 
2. a : 
3. a' : 
4. b : 
5. b' : 
6. a = a' mod m
7. b = b' mod m
8. a = b mod m
  a' = b' mod m
2 steps
2 1. m : 
2. a : 
3. a' : 
4. b : 
5. b' : 
6. a = a' mod m
7. b = b' mod m
8. a' = b' mod m
  a = b mod m
2 steps

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

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