Def outl == u:'a+'b. InjCase(u; x. x, arb('a))

is mentioned by

Thm* 'a,'b:S. all(x:hsum('a; 'b). implies(isl(x),equal(inl(outl(x)),x)))	[hinl_houtl]
Thm* 'a,'b:S. all(x:'a. equal(outl(inl(x)),x))	[houtl_wd]
Thm* 'a,'b:S, u:'a+'b. isl(u)  outl(u) = outl(u)	[houtl_nuprl]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html