Def implies == p:. q:. pq

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). (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. all(l:hlist('a). implies(not(null(l)),equal(cons(hd(l),tl(l)),l)))	[hcons_char]
Thm* 'a:S.  Thm* all Thm* (h1:'a. all Thm* (h1:'a. (h2:'a. implies Thm* (h1:'a. (h2:'a. (equal(h1,h2) Thm* (h1:'a. (h2:'a. ,all Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). all Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). implies Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (equal(l1,l2) Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,equal Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,(cons(h1,l1) Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ,,cons(h2,l2))))))))	[heq_list]
Thm* 'a:S.  Thm* all Thm* (h1:'a. all Thm* (h1:'a. (h2:'a. implies Thm* (h1:'a. (h2:'a. (not(equal(h1,h2)) Thm* (h1:'a. (h2:'a. ,all Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). all Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). not Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (equal Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ((cons(h1,l1) Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (,cons(h2,l2))))))))	[hnot_eq_list]
Thm* 'a:S.  Thm* all Thm* (l1:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). implies Thm* (l1:hlist('a). (l2:hlist('a). (not(equal(l1,l2)) Thm* (l1:hlist('a). (l2:hlist('a). ,all Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. all Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. not Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. (equal Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. ((cons(h1,l1) Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. (,cons(h2,l2))))))))	[hlist_not_eq]
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]

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

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