'a:S. 
  exists
  (rep:hlist('a)  hprod((hnum  'a); hnum). type_definition
  (rep:hlist('a)  hprod((hnum  'a); hnum). (is_list_rep
  (rep:hlist('a)  hprod((hnum  'a); hnum). ,rep))

1

1. 'a : S   rep:(hlist('a)  hprod((hnum  'a); hnum)).    type_definition(hprod((hnum  'a); hnum);hlist('a);is_list_rep;rep)

2 steps

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