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

is mentioned by

Thm* P:Prop{2}. (P)  P

[prop_to_bool_2_char]

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