Who Cites same range sep?
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
so_lambda2	Def  (1,2. b(1;2))(1,2) == b(1;2)
rev_implies	Def  P  Q == Q  P
	Thm*  A,B:Prop. (A  B)  Prop

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