1. 'a : S
  nil = abs_list(<n:hnum. @e:'a. true,0>)

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;nil;<n:. @e:'a. true,0>] THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

1	iso_pair('a List;('a);is_list_rep;rep_list;abs_list)	1 step
2	rep_list(nil) = <n:. @e:'a. true,0>  ('a)	5 steps

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