Some definitions of interest.
his_list_rep	Def is_list_rep Def == r:('a). f:'a Def == r:('a). n: Def == r:('a). (r Def == r:('a). = <m:. if m<n then f(m) else @x:'a. true fi ,n>)
	Thm* 'a:S. is_list_rep  (hprod((hnum  'a); hnum)  hbool)
bequal	Def x = y == (x = y  T)
	Thm* T:Type, x,y:T. (x = y)
habs_list	Def abs_list == r:('a). @a:'a List. (r = rep_list('a;a))
	Thm* 'a:S. abs_list  (hprod((hnum  'a); hnum)  hlist('a))
hbool	Def hbool ==
	Thm* hbool  S
hfun	Def 'a  'b == 'a'b
	Thm* 'a,'b:S. ('a  'b)  S
hlist	Def hlist('a) == 'a List
	Thm* 'a:S. hlist('a)  S
hnum	Def hnum ==
	Thm* hnum  S
hprod	Def hprod('a; 'b) == 'a'b
	Thm* 'a,'b:S. hprod('a; 'b)  S
hrep_list	Def rep_list == l:'a List. rep_list('a;l)
	Thm* 'a:S. rep_list  (hlist('a)  hprod((hnum  'a); hnum))
iso_pair	Def iso_pair('a;'b;P;rep;abs) Def == (r:'b. abs(r) = (@a:'a. (r = rep(a)))) & type_definition('b;'a;P;rep)
	Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a). Thm* iso_pair('a;'b;P;rep;abs)  Prop
label	Def t  ...$L == t
nat	Def  == {i:| 0i }
	Thm*   Type
	Thm*   S
stype	Def S == {T:Type| x:T. True }
	Thm* S  Type{2}

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