1. 'a : S
  (a:hlist('a). abs_list(rep_list(a)) = a)
  & (r:hprod((hnum  'a); hnum). 
  & (is_list_rep(r) = ((rep_list(abs_list(r))) = r)  hbool)

By:	((Inst ((Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a). ((Thm* iso_pair('a;'b;P;rep;abs) ((Thm*  ((Thm* (a:'a. abs(rep(a)) = a) & (r:'b. P(r) = ((rep(abs(r))) = r)) ((['a List;('a);is_list_rep;rep_list;abs_list]) (THEN (HN) THEN Try (Complete (Unfold `label` 0))

1

iso_pair('a List;('a);is_list_rep;rep_list;abs_list)

1 step

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