Some definitions of interest.
nat	Def  == {i:| 0i }
	Thm*   Type
nat_plus	Def  == {i:| 0<i }
	Thm*   Type
sfa_doc_exteq	Def A =ext B == (X:A. X  B) & (X:B. X  A)
sfa_doc_sexpr	Def Sexpr(A) == rec(T.(TT)+A)
	Thm* A:Type. Sexpr(A)  Type
sfa_doc_sexpr_reverse	Def Reverse(e) Def == Case of e Def == CaInj(x)  Inj(x) Def == CaCons(s1;s2)  Cons(Reverse(s2);Reverse(s1)) Def (recursive)
	Thm* A:Type, e:Sexpr(A). Reverse(e)  Sexpr(A)
sfa_doc_sexpr_size	Def Size(s) == Case of s :  Inj(x)  1 ; Cons(s1;s2)  Size(s1)+Size(s2) Def (recursive)
	Thm* A:Type, s:Sexpr(A). Size(s)
sfa_doc_sexpr_cases	Def Case of s :  Inj(x)  g(x) ; Cons(s1;s2)  f(s1;s2) Def == InjCase(s; s1s2. s1s2/s1,s2. f(s1;s2); x. g(x))
	Thm* A:Type, C:(Sexpr(A)Type), s:Sexpr(A), Thm* f:(s1,s2:Sexpr(A)C(Cons(s1;s2))), g:(x:AC(Inj(x))). Thm* (Case of s :  Inj(x)  g(x) ; Cons(s1;s2)  f(s1,s2))  C(s)
sfa_doc_sexpr_cons	Def Cons(s1;s2) == inl(<s1,s2>)
	Thm* A:Type, s1,s2:Sexpr(A). Cons(s1;s2)  Sexpr(A)
sfa_doc_sexpr_inj	Def Inj(a) == inr(a)
	Thm* A:Type, a:A. Inj(a)  Sexpr(A)
subtype	Def S  T == x:S. x  T

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