'a:S. 
  and
  (all(a:hlist('a). equal(abs_list(rep_list(a)),a))
  ,all
  ,(r:hprod((hnum  'a); hnum). equal
  ,(r:hprod((hnum  'a); hnum). (is_list_rep(r)
  ,(r:hprod((hnum  'a); hnum). ,equal(rep_list(abs_list(r)),r))))

1

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)

2 steps

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