Def R^+(x,y) == n:. x R^n y

is mentioned by

Thm* R:(TTProp), x,y:T. (x R^+ y)  (x R y)  (z:T. (x R^+ z) & (z R y))	[rel_plus_implies]
Thm* R:(TTProp). Trans x,y:T. x R^+ y	[rel_plus_trans]

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