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

1	(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 )	11 steps
2	||t||+1 = 2of(rep_list('a;t))+1	1 step

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