IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hres select wd1 1. 'a : S
2. P : 'a 3. B : 'a res_choose('a;x.P(x);x.B(x)) = (@x:'a. ((P(x))(B(x))))
By:
Unab [`bchoose`;`res_choose`] THEN Simp THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
res_choose('a;x.P(x);x.B(x)) = (@
x:'a. ((P(x))
(B(x))))
