IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hres abstract wd1 1. 'a : S
2. 'b : S
3. P : 'a 4. B : 'a'b res_lambda('a;'b;x.P(x);x.B(x)) = (x:'a. if P(x) then B(x) else arb('b) fi )
By:
Unab [`res_lambda`] THEN Simp THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
res_lambda('a;'b;x.P(x);x.B(x)) = (
x:'a. if P(x) then B(x) else arb('b) fi )
