(3steps 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 char 1

1. P : Prop
  InjCase(lem(P) ; true; false P


By: GenDC (lem(P)) THEN StrongAuto


Generated subgoal:

1 2. PVoid
3. P
  False

1 step

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

(3steps total) PrintForm Definitions hol Sections HOLlib Doc