(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 1

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


By: Analyze 0 THEN StrongAuto


Generated subgoal:

1 5. P(x)
  False

2 steps

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

(6steps total) PrintForm Definitions hol Sections HOLlib Doc