Who Cites houtl?
houtl	Def outl == u:'a+'b. InjCase(u; x. x, arb('a))
	Thm* 'a,'b:S. outl  (hsum('a; 'b)  'a)
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:

outl

has structure:

houtl('a; 'b)

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