Def hbool == 

is mentioned by

Thm* 'a:S.  Thm* all Thm* (P:hlist('a)  hbool. equal Thm* (P:hlist('a)  hbool. (all Thm* (P:hlist('a)  hbool. ((l:hlist('a). implies(equal(length(l),0),P(l))) Thm* (P:hlist('a)  hbool. ,P(nil)))	[hlength_eq_nil]
Thm* 'a:S.  Thm* all Thm* (P:hlist('a) Thm* ( hbool. all Thm* ( hbool. (n:hnum. equal Thm* ( hbool. (n:hnum. (all Thm* ( hbool. (n:hnum. ((l:hlist('a). implies(equal(length(l),suc(n)),P(l))) Thm* ( hbool. (n:hnum. ,all Thm* ( hbool. (n:hnum. ,(l:hlist('a). implies Thm* ( hbool. (n:hnum. ,(l:hlist('a). (equal(length(l),n) Thm* ( hbool. (n:hnum. ,(l:hlist('a). ,(l:hlist('a). all Thm* ( hbool. (n:hnum. ,(l:hlist('a). ,(l:hlist('a). (x:'a. P(cons(x,l)))) Thm* ( hbool. (n:hnum. ,(l:hlist('a). ,(l))))))	[hlength_eq_cons]
Thm* 'a:S.  Thm* all Thm* (l:hlist('a). all Thm* (l:hlist('a). (n:hnum. equal Thm* (l:hlist('a). (n:hnum. (equal(length(l),suc(n)) Thm* (l:hlist('a). (n:hnum. ,exists Thm* (l:hlist('a). (n:hnum. ,(h:'a. exists Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). and Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). (equal(length(l'),n) Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,equal Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,(l Thm* (l:hlist('a). (n:hnum. ,(h:'a. (l':hlist('a). ,,cons(h,l'))))))))	[hlength_cons_2]
Thm* 'a:S. all(l:hlist('a). equal(equal(length(l),0),equal(l,nil)))	[hlength_nil_2]
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* all Thm* (h:'a. all Thm* (h:'a. (t:hlist('a). all Thm* (h:'a. (t:hlist('a). (h':'a. all Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). equal Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). (equal Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ((cons(h,t) Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). (,cons(h',t')) Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ,and Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ,(equal(h,h') Thm* (h:'a. (t:hlist('a). (h':'a. (t':hlist('a). ,,equal(t,t')))))))	[hcons_11]
Thm* 'a:S.  Thm* all Thm* (P:hlist('a)  hbool. implies Thm* (P:hlist('a)  hbool. (and Thm* (P:hlist('a)  hbool. ((P(nil) Thm* (P:hlist('a)  hbool. (,all Thm* (P:hlist('a)  hbool. (,(t:hlist('a). implies Thm* (P:hlist('a)  hbool. (,(t:hlist('a). (P(t) Thm* (P:hlist('a)  hbool. (,(t:hlist('a). ,all(h:'a. P(cons(h,t)))))) Thm* (P:hlist('a)  hbool. ,all(l:hlist('a). P(l))))	[hlist_induct]
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]
Thm* 'a:S.  Thm* and Thm* (equal(null(nil),t) Thm* ,all(t:hlist('a). all(h:'a. equal(null(cons(h,t)),f))))	[hnull_def]

In prior sections: hol bool hol num hol pair hol prim rec hol restr binder hol list 1

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