T:Type, l:T List, a,x:T. (x  [a / l])  x = a  (x  l)

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

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