Nuprl - hol_list_1 LEMMAs for hlist_ty

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

Rank	Theorem	Name
8	Thm* 'a:S. Thm* exists Thm* (rep:hlist('a) hprod((hnum 'a); hnum). type_definition Thm* (rep:hlist('a) hprod((hnum 'a); hnum). (is_list_rep Thm* (rep:hlist('a) hprod((hnum 'a); hnum). ,rep))	[hlist_ty_def]
cites the following:
7	Thm* 'a:S. iso_pair('a List;('a);is_list_rep;rep_list;abs_list)	[list_iso]

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