(2steps total) PrintForm Definitions Lemmas hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hbool cases ax
  all(t:hbool. or(equal(t,t),equal(t,f)))
By: Simpsetp [`hol_to_nuprl`] THEN StrongAuto

Generated subgoal:

1 1. t : 
  t = true  t = false
1 step

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

(2steps total) PrintForm Definitions Lemmas hol bool Sections HOLlib Doc