Who Cites ho?
ho	Def o == f:'a'b. g:'a'b. f o g
	Thm* 'b,'c,'a:S. o  (('b  'c)  ('a  'b)  'a  'c)
compose	Def (f o g)(x) == f(g(x))
	Thm* A,B,C:Type, f:(BC), g:(AB). f o g  AC
tlambda	Def (x:T. b(x))(x) == b(x)

Syntax:

o

has structure:

ho('b; 'c; 'a)

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