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

1. T : S
2. P : T
3. x:TP(x)
  (x:TP(x))


By: Analyze 0 THEN StrongAuto


Generated subgoal:

1 4. x:TP(x)
  False

1 step

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

(6steps total) PrintForm Definitions hol Sections HOLlib Doc