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]
Def R^+(x,y) == n:. x R^n y	[rel_plus]

In prior sections: mb nat mb list 2 rel 1

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