1. T : Type
2. l : T List
3. a : T
4. x : T
5. i : 
6. i  0
7. 0<i
8. i<||l||+1
  x = [a / l][i]  x = a  (i:. i<||l|| & x = l[i])

By:	RWW Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0

1

9. x = l[(i-1)]   x = a  (i:. i<||l|| & x = l[i])

1 step

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