'a,'b:S, x:'a+'b. isl(x)  inl(outl(x)) = x

By:	RewriteOfThm Thm* 'a,'b:S. all(x:hsum('a; 'b). implies(isl(x),equal(inl(outl(x)),x))) HNC

1

1. 'a,'b:S, x:hsum('a; 'b). isl(x)  inl(outl(x)) = x   'a,'b:S, x:'a+'b. isl(x)  inl(outl(x)) = x

1 step

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