Nuprl - hol_list_2 Citations of stype

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def S == {T:Type|

x:T. True }

is mentioned by

Thm* 'a:S, h:'a, t:'a List, h':'a, t':'a List.
Thm* cons(h; t) = cons(h'; t')  h = h' & t = t' [cons_11_2]

Thm* 'a:S, P:(('a List)). (l:'a List. ||l|| = 0    P(l))  P(nil) [length_eq_nil]

Thm* 'a:S, P:(('a List)), n:.
Thm* (l:'a List. ||l|| = n+1    P(l))
Thm*
Thm* (l:'a List. ||l|| = n    (x:'a. P(cons(x; l)))) [length_eq_cons]

Thm* 'a:S, l:'a List, n:.
Thm* ||l|| = n+1    (h:'a, l':'a List. ||l'|| = n   & l = cons(h; l')) [length_cons_2]

Thm* 'a:S, l:'a List. ||l|| = 0    l = nil [length_nil_2]

Thm* 'a:S, Q,P:('a), l:'a List.
Thm* every(x:'a. (P(x))(Q(x));l)  every(P;l) & every(Q;l) [every_conj]

Thm* 'a:S, Q,P:('a), l:'a List.
Thm* every(x:'a. (P(x))(Q(x));l) = (every(P;l)every(Q;l)) [every_conj_2]

Thm* 'a:S, l:'a List, P:('a). every(P;l)  (n:. n<||l||  P(l[n])) [every_el]

Thm* 'b,'a:S, l:'a List, f:('a'b). ||map(f;l)|| = ||l||   [length_map]

Thm* 'a,'b:S, f:('a'b), l1,l2:'a List.
Thm* map(f;l1 @ l2) = (map(f;l1) @ map(f;l2)) [map_append_2]

Thm* 'a:S, l1,l2:'a List. ||l1 @ l2|| = ||l1||+||l2||   [length_append_2]

Thm* 'a:S, l1,l2,l3:'a List. (l1 @ (l2 @ l3)) = ((l1 @ l2) @ l3) [append_assoc_2]

Thm* 'a:S, l:'a List. mt(l)  cons(head(l); tl(l)) = l [cons_char]

Thm* 'a:S, h1,h2:'a.
Thm* h1 = h2  (l1,l2:'a List. l1 = l2  cons(h1; l1) = cons(h2; l2)) [eq_list]

Thm* 'a:S, h1,h2:'a. h1 = h2  (l1,l2:'a List. cons(h1; l1) = cons(h2; l2)) [not_eq_list]

Thm* 'a:S, l1,l2:'a List. l1 = l2  (h1,h2:'a. cons(h1; l1) = cons(h2; l2)) [list_not_eq]

Thm* 'a:S, t:'a List, h:'a. cons(h; t) = nil  False [not_cons_nil2]

Thm* 'a:S, t:'a List, h:'a. cons(h; t) = nil [not_cons_nil]

Thm* 'a:S, t:'a List, h:'a. nil = cons(h; t)  False [not_nil_cons2]

Thm* 'a:S, t:'a List, h:'a. nil = cons(h; t) [not_nil_cons]

Thm* 'a:S, h:'a, t:'a List, h':'a, t':'a List.
Thm* cons(h; t) = cons(h'; t')  h = h' & t = t' [cons_11]

Thm* 'a:S, l:'a List. l = nil  (t:'a List, h:'a. l = cons(h; t)) [list_cases]

Thm* 'a:S, P:(('a List)).
Thm* P(nil) & (t:'a List. P(t)  (h:'a. P(cons(h; t))))  (l:'a List. P(l)) [list_induct]

Thm* 'a:S. True & (h:'a, t:'a List. True) [null_char]

Thm* 'b,'a:S, x:'b, f:('b'a('a List)'b).
Thm* (fn1:(('a List)'b).
Thm* (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t)))
Thm* & (fn1,y:(('a List)'b).
Thm* & (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t))
Thm* & (& y(nil) = x
Thm* & (& (h:'a, t:'a List. y(cons(h; t)) = f(y(t),h,t))
Thm* & (
Thm* & (fn1 = y) [list_axiom]

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* 'b,'a:S.
Thm* all(l:hlist('a). all(f:'a  'b. equal(length(map(f,l)),length(l)))) [hlength_map]

Thm* 'a,'b:S.
Thm* all
Thm* (f:'a  'b. all
Thm* (f:'a  'b. (l1:hlist('a). all
Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). equal
Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). (map(f,append(l1,l2))
Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). ,append
Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). ,(map(f,l1)
Thm* (f:'a  'b. (l1:hlist('a). (l2:hlist('a). ,,map(f,l2)))))) [hmap_append_2]

Thm* 'a:S.
Thm* all
Thm* (l1:hlist('a). all
Thm* (l1:hlist('a). (l2:hlist('a). equal
Thm* (l1:hlist('a). (l2:hlist('a). (length(append(l1,l2))
Thm* (l1:hlist('a). (l2:hlist('a). ,add(length(l1),length(l2))))) [hlength_append_2]

Thm* 'a:S.
Thm* all
Thm* (l1:hlist('a). all
Thm* (l1:hlist('a). (l2:hlist('a). all
Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). equal
Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). (append(l1,append(l2,l3))
Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,append
Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,(append(l1,l2)
Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,,l3))))) [happend_assoc_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: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]

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* '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]

In prior sections: hol hol min hol bool 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

hol list 2 Sections HOLlib Doc

Thm* 'a:S, h:'a, t:'a List, h':'a, t':'a List. Thm* cons(h; t) = cons(h'; t') h = h' & t = t'	[cons_11_2]
Thm* 'a:S, P:(('a List)). (l:'a List. \|\|l\|\| = 0 P(l)) P(nil)	[length_eq_nil]
Thm* 'a:S, P:(('a List)), n:. Thm* (l:'a List. \|\|l\|\| = n+1 P(l)) Thm* Thm* (l:'a List. \|\|l\|\| = n (x:'a. P(cons(x; l))))	[length_eq_cons]
Thm* 'a:S, l:'a List, n:. Thm* \|\|l\|\| = n+1 (h:'a, l':'a List. \|\|l'\|\| = n & l = cons(h; l'))	[length_cons_2]
Thm* 'a:S, l:'a List. \|\|l\|\| = 0 l = nil	[length_nil_2]
Thm* 'a:S, Q,P:('a), l:'a List. Thm* every(x:'a. (P(x))(Q(x));l) every(P;l) & every(Q;l)	[every_conj]
Thm* 'a:S, Q,P:('a), l:'a List. Thm* every(x:'a. (P(x))(Q(x));l) = (every(P;l)every(Q;l))	[every_conj_2]
Thm* 'a:S, l:'a List, P:('a). every(P;l) (n:. n<\|\|l\|\| P(l[n]))	[every_el]
Thm* 'b,'a:S, l:'a List, f:('a'b). \|\|map(f;l)\|\| = \|\|l\|\|	[length_map]
Thm* 'a,'b:S, f:('a'b), l1,l2:'a List. Thm* map(f;l1 @ l2) = (map(f;l1) @ map(f;l2))	[map_append_2]
Thm* 'a:S, l1,l2:'a List. \|\|l1 @ l2\|\| = \|\|l1\|\|+\|\|l2\|\|	[length_append_2]
Thm* 'a:S, l1,l2,l3:'a List. (l1 @ (l2 @ l3)) = ((l1 @ l2) @ l3)	[append_assoc_2]
Thm* 'a:S, l:'a List. mt(l) cons(head(l); tl(l)) = l	[cons_char]
Thm* 'a:S, h1,h2:'a. Thm* h1 = h2 (l1,l2:'a List. l1 = l2 cons(h1; l1) = cons(h2; l2))	[eq_list]
Thm* 'a:S, h1,h2:'a. h1 = h2 (l1,l2:'a List. cons(h1; l1) = cons(h2; l2))	[not_eq_list]
Thm* 'a:S, l1,l2:'a List. l1 = l2 (h1,h2:'a. cons(h1; l1) = cons(h2; l2))	[list_not_eq]
Thm* 'a:S, t:'a List, h:'a. cons(h; t) = nil False	[not_cons_nil2]
Thm* 'a:S, t:'a List, h:'a. cons(h; t) = nil	[not_cons_nil]
Thm* 'a:S, t:'a List, h:'a. nil = cons(h; t) False	[not_nil_cons2]
Thm* 'a:S, t:'a List, h:'a. nil = cons(h; t)	[not_nil_cons]
Thm* 'a:S, h:'a, t:'a List, h':'a, t':'a List. Thm* cons(h; t) = cons(h'; t') h = h' & t = t'	[cons_11]
Thm* 'a:S, l:'a List. l = nil (t:'a List, h:'a. l = cons(h; t))	[list_cases]
Thm* 'a:S, P:(('a List)). Thm* P(nil) & (t:'a List. P(t) (h:'a. P(cons(h; t)))) (l:'a List. P(l))	[list_induct]
Thm* 'a:S. True & (h:'a, t:'a List. True)	[null_char]
Thm* 'b,'a:S, x:'b, f:('b'a('a List)'b). Thm* (fn1:(('a List)'b). Thm* (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t))) Thm* & (fn1,y:(('a List)'b). Thm* & (fn1(nil) = x & (h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t)) Thm* & (& y(nil) = x Thm* & (& (h:'a, t:'a List. y(cons(h; t)) = f(y(t),h,t)) Thm* & ( Thm* & (fn1 = y)	[list_axiom]
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* 'b,'a:S. Thm* all(l:hlist('a). all(f:'a 'b. equal(length(map(f,l)),length(l))))	[hlength_map]
Thm* 'a,'b:S. Thm* all Thm* (f:'a 'b. all Thm* (f:'a 'b. (l1:hlist('a). all Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). equal Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). (map(f,append(l1,l2)) Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). ,append Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). ,(map(f,l1) Thm* (f:'a 'b. (l1:hlist('a). (l2:hlist('a). ,,map(f,l2))))))	[hmap_append_2]
Thm* 'a:S. Thm* all Thm* (l1:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). equal Thm* (l1:hlist('a). (l2:hlist('a). (length(append(l1,l2)) Thm* (l1:hlist('a). (l2:hlist('a). ,add(length(l1),length(l2)))))	[hlength_append_2]
Thm* 'a:S. Thm* all Thm* (l1:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). equal Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). (append(l1,append(l2,l3)) Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,append Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,(append(l1,l2) Thm* (l1:hlist('a). (l2:hlist('a). (l3:hlist('a). ,,l3)))))	[happend_assoc_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: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]
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* '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]