Who Cites houtr?
houtr	Def outr == u:'a+'b. InjCase(u; x. arb('b), x)
	Thm* 'a,'b:S. outr  (hsum('a; 'b)  'b)
arb	Def arb(T) == InjCase(lem(T); x. x, "uu")
	Thm* T:S. arb(T)  T
tlambda	Def (x:T. b(x))(x) == b(x)

Syntax:

outr

has structure:

houtr('a; 'b)

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