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''||
  x' = x''

By:	Assert ((i:||x'||. x'[i]){||x'||} = (i:||x''||. x''[i]){||x''||}) THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

1	(i:||x'||. x'[i]){||x'||} = (i:||x''||. x''[i]){||x''||}	5 steps
2	6. (i:||x'||. x'[i]){||x'||} = (i:||x''||. x''[i]){||x''||}   x' = x''	1 step

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