Nuprl - Proof: houtr wd

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

'b,'a:S. all(

x:'b. equal(outr(inr(x)),x))

By:	Unab [`houtr`] THEN HN THEN StrongAuto

Generated subgoals:

None

About:

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