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

Generated subgoal:

1 3. XM
4. (x:T. P(x))
5. x : T
  P(x)
2 steps

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

(9steps total) PrintForm Definitions hol Sections HOLlib Doc