1. 'a : S
2. x' : 'a List
3. n : 
  if n<||x'|| then x'[n] else arb('a) fi 
  =
  if n<||x'||
  then if n<||x'|| then x'[n] else arb('a) fi 
  else @x:'a. true
  fi 

1

4. n<||x'||   arb('a) = (@x:'a. true)

1 step

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