(3steps total) PrintForm Definitions hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hnot def 1
  (p:. p) = (t:. tfalse)
By: ((Simpset [`ext`]) THEN (Simpset [`bequal`])) THEN Simp THEN StrongAuto

Generated subgoal:

1 1. t : 
2. t  False
  t
1 step

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

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