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

1

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

2 steps

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