(7steps total) PrintForm Definitions hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hforall def 1 1 1 1
1. 'a : S
2. P : 'a
3. x:'a. P(x)
4. x : 'a
  P(x) = true
By: Simpset [`bequal`] THEN StrongAuto THEN Simp THEN StrongAuto

Generated subgoal:

1 5. True
  P(x)
1 step

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

(7steps total) PrintForm Definitions hol bool Sections HOLlib Doc