Who Cites hone one?
hone_one	Def one_one == f:'a'b. one_one('a;'b;f)
	Thm* 'a,'b:S. one_one  (('a  'b)  hbool)
one_one	Def one_one('a;'b;f) == x,y:'a. f(x) = f(y)  'b  x = y
	Thm* 'a,'b:Type, f:('a'b). one_one('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:

one_one

has structure:

hone_one('a; 'b)

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