Who Cites eqmod?
eqmod	Def a = b mod m == m | a-b
	Thm* m,a,b:. (a = b mod m)  Prop
divides	Def b | a == c:. a = bc
	Thm* a,b:. (a | b)  Prop

Syntax:

a = b mod m

has structure:

eqmod(m; a; b)

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