is mentioned by

Thm* x,y:A, P:(AProp), i,j:. Thm* P(if i=j x else y fi)  P(if i=j x else y fi)	[eq_int_cases_test]
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