Some definitions of interest.
equiv_rel_sep	Def  EquivRel on A, R == EquivRel u,v:A. R(u;v)
same_range_sep	Def  same_range_sep(A; B) == f,g. j:B. (i:A. f(i) = j)  (i:A. g(i) = j)
	Thm*  same_range_sep(A; B)  (AB)(AB)Prop
	Thm*  same_range_sep(A; B)  (A inj B)(A inj B)Prop
iff	Def  P  Q == (P  Q) & (P  Q)
	Thm*  A,B:Prop. (A  B)  Prop

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