(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