Def R1 => R2 == x,y:T. (x R1 y)  (x R2 y)

is mentioned by

Thm* R1,R2:(TTProp), x,y:T. R1 => R2  (x (R1^*) y)  (x (R2^*) y)	[rel_star_monotonic]
Thm* R1,R2:(TTProp). R1 => R2  R1^* => R2^*	[rel_star_monotone]
Thm* n:, T:Type, R1,R2:(TTProp). R1 => R2  R1^n => R2^n	[rel_exp_monotone]

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