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

1

(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 )

3 steps

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