Def  same_range_sep(A; B) == f,g. j:B. (i:A. f(i) = j)  (i:A. g(i) = j)

is mentioned by

Thm*  EquivRel on A inj B, same_range_sep(A; B)	[same_range_sep_inj_eqv]
Thm*  EquivRel on AB, same_range_sep(A; B)	[same_range_sep_eqv]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html