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

By:	((DTerm (n.if n<||x'|| then x'[n] else arb('a) fi ) 0) THEN (DTerm ||x'|| 0)) THEN Simp THEN StrongAuto THEN Id THEN Simp THEN StrongAuto

1

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

4 steps

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