(3steps total) PrintForm Definitions hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hf def
  equal(f,all(t:hbool. t))
By: Simpset [`hol_to_nuprl`] THEN Simp THEN StrongAuto

Generated subgoal:

1   false = (t:. t)
2 steps

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

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