1. 'a : S
2. h : 'a
3. t : hlist('a)
  rep_list(cons(h; t))
  =
  <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 ,||t||+1>   =   <m:. if m = 0 then h else 1of(rep_list('a;t))(pre(m)) fi    ,2of(rep_list('a;t))+1>    ('a)

13 steps

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