1. T : Type
2. x : T
3. L : T List
4. P : TTProp
5. i:||L||, j:i. P(L[j],L[i])
6. y:T. (y  L)  P(x,y)
7. i : ||[x / L]||
8. j : i
9. j = 0
  (L[(i-1)]  L)

By:	BackThru Thm* L:T List, i:||L||. (L[i]  L)

None

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