Nuprl - hol_list_2 LEMMAs for every

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

Theorem	Name
Thm* 'a:S, l:'a List, P:('a). every(P;l) (n:. n<\|\|l\|\| P(l[n]))	[every_el]
cites the following:
Thm* 'a:S. Thm* all Thm* (l:hlist('a). all Thm* (l:hlist('a). (P:'a hbool. equal Thm* (l:hlist('a). (P:'a hbool. (every(P,l) Thm* (l:hlist('a). (P:'a hbool. ,all Thm* (l:hlist('a). (P:'a hbool. ,(n:hnum. implies Thm* (l:hlist('a). (P:'a hbool. ,(n:hnum. (lt(n,length(l)) Thm* (l:hlist('a). (P:'a hbool. ,(n:hnum. ,P(el(n,l)))))))	[hevery_el]

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