is mentioned by

Thm* a,b:. (a -- b) = 0  ab	[ndiff_zero]
Thm* a,b:. (a -- b)+b = imax(a;b)	[ndiff_add_eq_imax]
Thm* a,b:. (a -- (a -- b)) = imin(a;b)	[ndiff_ndiff_eq_imin]
Thm* a,b:, c:. ((a -- b) -- c) = (a -- (b+c))	[ndiff_ndiff]
Thm* a:, b:. ((a+b) -- b) = a	[ndiff_inv]
Thm* a:. (0 -- a) = 0	[ndiff_ann_l]
Thm* a:. (a -- 0) = a	[ndiff_id_r]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html