Def append == l1:'a List. l2:'a List. l1 @ l2

is mentioned by

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.  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]

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