is mentioned by

Thm* 'a,'b:S, x:'a+'b. isr(x)  inr(outr(x)) = x	[inr_houtr]
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