Nuprl - hol_list_2 LEMMAs for list

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Theorem	Name
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]
cites the following:
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]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html