Some definitions of interest.
bchoose	Def @x:'a. p(x) == @x:'a. p(x)
	Thm* 'a:S, p:('a). (@x:'a. p(x))  'a
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)
res_choose	Def res_choose('a;x.P(x);x.Q(x)) == @x:'a. (P(x) & Q(x))
	Thm* 'a:S, P,Q:('aProp). res_choose('a;x.P(x);x.Q(x))  'a
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