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