is mentioned by

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 list 1

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