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

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


By: DTerm x 0 THEN StrongAuto


Generated subgoals:

None

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

(6steps total) PrintForm Definitions hol Sections HOLlib Doc