1. 'a : S
2. x : ('a)
3. f : 'a
4. n : 
5. x = <m:. if m<n then f(m) else @x:'a. true fi ,n>
6. ||f{n}|| = n-0
  (m:. if m<n then f(m) else @x:'a. true fi )
  =
  (n@0:. if n@0<||f{n}|| then (f{n})[n@0] else arb('a) fi )

1

7. m :    if m<n then f(m) else @x:'a. true fi    =   if m<||f{n}|| then (f{n})[m] else arb('a) fi

5 steps

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