1. 'a : S
2. h : 'a
3. t : hlist('a)
  (n:. if n<||t||+1 then cons(h; t)[n] else arb('a) fi )
  =
  (m:. if m = 0 then h else 1of(rep_list('a;t))(pre(m)) fi )

1

4. n :    if n<||t||+1 then cons(h; t)[n] else arb('a) fi    =   if n = 0 then h else 1of(rep_list('a;t))(pre(n)) fi

10 steps

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