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* n:, R:(nnProp), x,y:n. (x (R^*) y)  (k:(n+1). x R^k y)	[rel_star_finite]
Thm* R:(TTProp), k:, x,y:T. Thm* (x R^k y) Thm*  Thm* (L:T List.  Thm* (||L|| = k+1   & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))	[rel_exp_list]

In prior sections: mb nat

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