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

is mentioned by

Thm* 'a,'b:S. all(x:hsum('a; 'b). implies(isr(x),equal(inr(outr(x)),x)))	[hinr_houtr]
Thm* 'b,'a:S. all(x:'b. equal(outr(inr(x)),x))	[houtr_wd]
Thm* 'a,'b:S, u:'a+'b. isr(u)  outr(u) = outr(u)	[houtr_nuprl]

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