(3steps 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 weakening
  m,a,b:. a = b  (a = b mod m)
By: Unfold `eqmod` 0 THEN UnivCD

Generated subgoal:

1 1. m : 
2. a : 
3. b : 
4. a = b
  m | a-b
2 steps

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

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