IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hres forall wd1 1. 'a : S
2. P : 'a 3. B : 'a (res_all('a;x.P(x);x.B(x))) = (x:'a. (P(x))(B(x)))
By:
Unab [`res_all`] THEN Simpsetp [`bequal`] THEN StrongAuto THEN Try HypBackchain
THEN
StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(
res_all('a;x.P(x);x.B(x))) = (
(B(x)))
