(4steps total) PrintForm Definitions Lemmas hol one Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hone def 1
   = (@x:Unit. true)
By: Unab [`bchoose`] THEN ChooseDC THEN StrongAuto

Generated subgoals:

1 1. x : Unit
2. True
   = x
1 step
2   x:Unit. True
1 step

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

(4steps total) PrintForm Definitions Lemmas hol one Sections HOLlib Doc