1. T : Type
2. l1 : T List
3. l2 : T List
4. x : T
5. ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])
6. i:. i<||l1|| & x = l1[i]
  i:. i<||l2|| & x = l2[i]

1

5. ||l1||||l2|| 6. i:. i<||l1||  l1[i] = l2[i] 7. i :  8. i<||l1|| 9. x = l1[i]   x = l2[i]

1 step

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