'a:S. iso_pair('a List;('a);is_list_rep;rep_list;abs_list)

1	1. 'a : S 2. r : ('a)   abs_list(r) = (@a:'a List. (r = rep_list(a)  ('a)))	1 step
2	1. 'a : S   type_definition(('a);'a List;is_list_rep;rep_list)	35 steps

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