Def P == InjCase(lem(P) ; true; false)

is mentioned by

Thm* P:. (P) = P	[prop_to_bool_char_2]
Thm* (P)  P	[prop_to_bool_char]
Def x = y == (x = y  T)	[bequal]
Def x:T. P(x) == (x:T. P(x))	[bexists]
Def x:T. P(x) == (x:T. P(x))	[ball]

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