Def R^n == if n=0 x,y. x = y  T else x,y. z:T. (x R z) & (z R^n-1 y) fi
Def (recursive)

is mentioned by

Thm* R:(TTProp), n:, x,y:T. (x R^n^-1 y)  (x R^-1^n y)	[rel_inverse_exp]
Thm* n:, T:Type, R1,R2:(TTProp). R1 => R2  R1^n => R2^n	[rel_exp_monotone]
Thm* R:(TTProp), m,n:, x,y,z:T. (x R^m y)  (y R^n z)  (x R^m+n z)	[rel_exp_add]
Thm* k,n:, R:(nnProp). (i,j:n. Dec(i R j))  (i,j:n. Dec(i R^k j))	[decidable__rel_exp]
Def (R^*)(x,y) == n:. x R^n y	[rel_star]

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