Def lt == m:. n:. m<n

is mentioned by

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]

In prior sections: hol prim rec hol list 1

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