1. T : Type
2. R : TTProp
3. k : 
4. 0<k
5. x,y:T.
5. (x R^k-1 y)
5. 
5. (L:T List. 
5. (||L|| = k-1+1 & L[0] = x & last(L) = y & (i:(k-1). L[i] R L[(i+1)]))
6. k = 0
7. T
8. T
9. L : T List
10. ||L|| = k+1
  null(L)

By:	(RW assert_pushdownC 0) THEN (RWO Thm* as:A List. as = nil  ||as||1 0)

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html