Who Cites hinl?
hinl	Def inl == x:'a. inl(x)
	Thm* 'a,'b:S. inl  ('a  hsum('a; 'b))
tlambda	Def (x:T. b(x))(x) == b(x)

Syntax:

inl

has structure:

hinl('a; 'b)

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