1. T : Type
2. L : T List
3. x : T
4. i : {1..(||L||+1)}
5. j : {1..(||L||+1)}
6. i1 : 
7. i1<||[x / L]||
8. i1 = 0
9. n : ||L||
10. (i-1, j-1)(i1-1) = n
  [x / L][(n+1)] = L[n]

By:	RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0 THEN Try (Complete Auto)

None

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