is mentioned by

Thm* x,y:. x=y  x = y	[assert_of_eq_int_rw]
Thm* u,v:. uv  u  v	[assert_functionality_wrt_bimplies]
Thm* P:(Prop). P(false)  P(true)  (b:. P(b))	[bool_ind]

In prior sections: core well fnd int 1

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