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

is mentioned

In prior sections: DiscreteMath

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