Who Cites harb?
harb	Def arb == arb('a)
	Thm* 'a:S. arb  'a
arb	Def arb(T) == InjCase(lem(T); x. x, "uu")
	Thm* T:S. arb(T)  T

Syntax:

arb

has structure:

harb('a)

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