Def every == p:'a. l:'a List. every(p;l)

is mentioned by

Thm* 'a:S.  Thm* all Thm* (Q:'a  hbool. all Thm* (Q:'a  hbool. (P:'a  hbool. all Thm* (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). equal Thm* (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). (every Thm* (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). (((x:'a. and(P(x),Q(x))) Thm* (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). (,l) Thm* (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). ,and Thm* (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). ,(every(P,l) Thm* (Q:'a  hbool. (P:'a  hbool. (l:hlist('a). ,,every(Q,l))))))	[hevery_conj]
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]
Thm* 'a:S.  Thm* and Thm* (all(P:'a  hbool. equal(every(P,nil),t)) Thm* ,all Thm* ,(P:'a  hbool. all Thm* ,(P:'a  hbool. (h:'a. all Thm* ,(P:'a  hbool. (h:'a. (t:hlist('a). equal Thm* ,(P:'a  hbool. (h:'a. (t:hlist('a). (every(P,cons(h,t)) Thm* ,(P:'a  hbool. (h:'a. (t:hlist('a). ,and(P(h),every(P,t)))))))	[hevery_def]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html