(6steps total) PrintForm Definitions hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prop to bool 2 char 1

1. P : Prop
  (P P


By: Unab [`prop_to_bool_2`]


Generated subgoal:

1   InjCase(lem_2(P) ; true; false P
4 steps

About:
bfalsebtrueassertdecideapplyprop
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(6steps total) PrintForm Definitions hol Sections HOLlib Doc