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

By:

Inst Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a), a:'a, r:'b. Thm* iso_pair('a;'b;P;rep;abs)  rep(a) = r  a = abs(r) ['a List ;('a) ;is_list_rep ;rep_list ;abs_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>] THEN Try (Complete (Unfold `label` 0))

1	iso_pair('a List;('a);is_list_rep;rep_list;abs_list)	1 step
2	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)	14 steps

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