Def cons == x:'a. l:'a List. cons(x; l)

is mentioned by

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). 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. all(t:hlist('a). all(h:'a. not(equal(cons(h,t),nil))))	[hnot_cons_nil]
Thm* 'a:S. all(t:hlist('a). all(h:'a. not(equal(nil,cons(h,t)))))	[hnot_nil_cons]
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* (l:hlist('a). or Thm* (l:hlist('a). (equal(l,nil) Thm* (l:hlist('a). ,exists(t:hlist('a). exists(h:'a. equal(l,cons(h,t))))))	[hlist_cases]
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. and(null(nil),all(h:'a. all(t:hlist('a). not(null(cons(h,t))))))	[hnull_char]
Thm* 'b,'a:S. Thm* all Thm* (x:'b. all Thm* (x:'b. (f:'b Thm* (x:'b. ( 'a Thm* (x:'b. ( hlist('a) Thm* (x:'b. ( 'b. exists_unique Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. and Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. (equal(fn1(nil),x) Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,all Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. all Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). equal Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). (fn1 Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ((cons(h,t)) Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,f Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,(fn1(t) Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,,h Thm* (x:'b. ( 'b. (fn1:hlist('a)  'b. ,(h:'a. (t:hlist('a). ,,t))))))))	[hlist_axiom]
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,'b,'c:S. Thm* and Thm* (all(f:'a  'b  'c. equal(map2(f,nil,nil),nil)) Thm* ,all Thm* ,(f:'a Thm* ,( 'b Thm* ,( 'c. all Thm* ,( 'c. (h1:'a. all Thm* ,( 'c. (h1:'a. (t1:hlist Thm* ,( 'c. (h1:'a. (('a). all Thm* ,( 'c. (h1:'a. (('a). (h2:'b. all Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). equal Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (map2 Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ((f Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (,cons(h1,t1) Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). (,cons(h2,t2)) Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,cons Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,(f(h1,h2) Thm* ,( 'c. (h1:'a. (('a). (h2:'b. (t2:hlist('b). ,,map2(f,t1,t2)))))))))	[hmap2_wd]
Thm* 'a,'b:S. Thm* and Thm* (all(f:'a  'b. equal(map(f,nil),nil)) Thm* ,all Thm* ,(f:'a  'b. all Thm* ,(f:'a  'b. (h:'a. all Thm* ,(f:'a  'b. (h:'a. (t:hlist('a). equal Thm* ,(f:'a  'b. (h:'a. (t:hlist('a). (map(f,cons(h,t)) Thm* ,(f:'a  'b. (h:'a. (t:hlist('a). ,cons(f(h),map(f,t)))))))	[hmap_wd]
Thm* 'a:S.  Thm* and Thm* (equal(length(nil),0) Thm* ,all(h:'a. all(t:hlist('a). equal(length(cons(h,t)),suc(length(t))))))	[hlength_wd]
Thm* 'a:S.  Thm* and Thm* (equal(flat(nil),nil) Thm* ,all Thm* ,(h:hlist('a). all Thm* ,(h:hlist('a). (t:hlist(hlist('a)). equal Thm* ,(h:hlist('a). (t:hlist(hlist('a)). (flat(cons(h,t)) Thm* ,(h:hlist('a). (t:hlist(hlist('a)). ,append(h,flat(t))))))	[hflat_wd]
Thm* 'a:S.  Thm* and Thm* (all(l:hlist('a). equal(append(nil,l),l)) Thm* ,all Thm* ,(l1:hlist('a). all Thm* ,(l1:hlist('a). (l2:hlist('a). all Thm* ,(l1:hlist('a). (l2:hlist('a). (h:'a. equal Thm* ,(l1:hlist('a). (l2:hlist('a). (h:'a. (append(cons(h,l1),l2) Thm* ,(l1:hlist('a). (l2:hlist('a). (h:'a. ,cons(h,append(l1,l2)))))))	[happend_wd]
Thm* and Thm* (equal(it_sum(nil),0) Thm* ,all Thm* ,(h:hnum. all(t:hlist(hnum). equal(it_sum(cons(h,t)),add(h,it_sum(t))))))	[hit_sum_wd]
Thm* 'a:S. all(t:hlist('a). all(h:'a. equal(tl(cons(h,t)),t)))	[htl_wd]
Thm* 'a:S. all(t:hlist('a). all(h:'a. equal(hd(cons(h,t)),h)))	[hhd_wd]
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]
Thm* 'a:S.  Thm* all Thm* (h:'a. all Thm* (h:'a. (t:hlist('a). equal Thm* (h:'a. (t:hlist('a). (cons(h,t) Thm* (h:'a. (t:hlist('a). ,abs_list Thm* (h:'a. (t:hlist('a). ,(pair Thm* (h:'a. (t:hlist('a). ,(((m:hnum. cond Thm* (h:'a. (t:hlist('a). ,(((m:hnum. (equal(m,0) Thm* (h:'a. (t:hlist('a). ,(((m:hnum. ,h Thm* (h:'a. (t:hlist('a). ,(((m:hnum. ,fst(rep_list(t),pre(m)))) Thm* (h:'a. (t:hlist('a). ,(,suc(snd(rep_list(t))))))))	[hcons_def]

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