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

1

8. i<||l||+1   x = [a / l][i]  x = a  (i:. i<||l|| & x = l[i])

2 steps

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