(9steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc sample intmod wf
  k:.  mod k  Type
By: Def of  mod k

Generated subgoal:

1 1. k : 
  EquivRel x,y:. m:. x-y = mk
8 steps

About:
intsubtractmultiplyuniverseequalmemberallexists
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(9steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Search Doc