T:Type, l1,l2:T List.
  l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])

1	1. T : Type 2. T List   l2:T List. nil  l2  ||nil||||l2|| & (i:. i<||nil||  nil[i] = l2[i])	1 step
2	1. T : Type 2. T List 3. u : T 4. v : T List 5. l2:T List. v  l2  ||v||||l2|| & (i:. i<||v||  v[i] = l2[i])   l2:T List.    [u / v]  l2      ||[u / v]||||l2|| & (i:. i<||[u / v]||  [u / v][i] = l2[i])	17 steps

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