(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 1
1. P : Prop
  v:P+(PVoid). InjCase(v ; true; false)  P
By: (Analyze 0) THEN (Last Analyze) THEN (Reduce 0)

Generated subgoal:

1 2. PVoid
3. P
  False
1 step

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

(6steps total) PrintForm Definitions hol Sections HOLlib Doc