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

Generated subgoals:

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

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

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