'a:S. 
  all
  (h:'a. all
  (h:'a. (t:hlist('a). equal
  (h:'a. (t:hlist('a). (cons(h,t)
  (h:'a. (t:hlist('a). ,abs_list
  (h:'a. (t:hlist('a). ,(pair
  (h:'a. (t:hlist('a). ,(((m:hnum. cond
  (h:'a. (t:hlist('a). ,(((m:hnum. (equal(m,0)
  (h:'a. (t:hlist('a). ,(((m:hnum. ,h
  (h:'a. (t:hlist('a). ,(((m:hnum. ,fst(rep_list(t),pre(m))))
  (h:'a. (t:hlist('a). ,(,suc(snd(rep_list(t))))))))

1

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

16 steps

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