Nuprl - Proof: hone def

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hone def

equal(one_el,select(

x:hone. t))

By:	HN THEN StrongAuto

Generated subgoal:

1 = (@x:Unit. true)
3 steps

About:

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