Def a  b  T == a = b  T

is mentioned by

Thm* i,j:. (i=j) = false  i  j	[eq_int_eq_false_elim]
Thm* i,j:. i  j  (i=j) = false	[eq_int_eq_false]
Thm* x,y:Atom. x=yAtom  x  y	[neg_assert_of_eq_atom]
Thm* x,y:. x=y  x  y	[neg_assert_of_eq_int]

In prior sections: int 1

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