Nuprl - hol_bool LEMMAs for hcond

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

Theorem	Name
Thm* 'a:S. Thm* equal Thm* (cond Thm* ,t:hbool. t1:'a. t2:'a. select Thm* ,t:hbool. t1:'a. t2:'a. (x:'a. and Thm* ,t:hbool. t1:'a. t2:'a. (x:'a. (implies(equal(t,t),equal(x,t1)) Thm* ,t:hbool. t1:'a. t2:'a. (x:'a. ,implies(equal(t,f),equal(x,t2)))))	[hcond_def]
cites the following:
Thm* P:('aType), x:'a. P(x) (y:'a. P(y) x = y) (@y:'a. P(y)) = x	[choose_unique]

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