Def el == n:. l:'a List. if n=0 then hd(l) else el(n-1,tl(l)) fi 
Def (recursive)

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]
Thm* 'a:S.  Thm* and Thm* (all(l:hlist('a). equal(el(0,l),hd(l))) Thm* ,all(l:hlist('a). all(n:hnum. equal(el(suc(n),l),el(n,tl(l))))))	[hel_wd]

In prior sections: hol list 1

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