(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
1. T : S
2. P : T
3. x:T. P(x)
4. x:T. P(x)
  False
By: Analyze 4 THEN DTerm x 3 THEN StrongAuto

Generated subgoals:

None

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

(6steps total) PrintForm Definitions hol Sections HOLlib Doc