Who Cites honto?
honto	Def onto == f:'a'b. onto('a;'b;f)
	Thm* 'a,'b:S. onto  (('a  'b)  hbool)
onto	Def onto('a;'b;f) == y:'b. x:'a. y = f(x)
	Thm* 'a,'b:Type, f:('a'b). onto('a;'b;f)  Prop
prop_to_bool	Def P == InjCase(lem(P) ; true; false)
	Thm* P:Prop. (P)
tlambda	Def (x:T. b(x))(x) == b(x)

Syntax:

onto

has structure:

honto('a; 'b)

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