(9steps total) PrintForm Definitions hol Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bnot ball 1 1 1 1 1
1. T : S
2. P : T
3. XM
4. (x:T. P(x))
5. x : T
6. P(x)
  P(x)
By: Analyze 4 THEN StrongAuto THEN DTerm x 0 THEN StrongAuto

Generated subgoals:

None

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

(9steps total) PrintForm Definitions hol Sections HOLlib Doc