1. 'a : S
2. x' : 'a List
3. x'' : 'a List
4. (n:. if n<||x'|| then x'[n] else arb('a) fi )
4. =
4. (n:. if n<||x''|| then x''[n] else arb('a) fi )
5. ||x'|| = ||x''||
6. i : ||x'||
  x'[i] = x''[i]

1

4. ||x'|| = ||x''||   5. i : ||x'|| 6. if i<||x'|| then x'[i] else arb('a) fi  6. = 6. if i<||x''|| then x''[i] else arb('a) fi    x'[i] = x''[i]

2 steps

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