'a:S, l:'a List. mt(l)  cons(head(l); tl(l)) = l

By:	RewriteOfThm Thm* 'a:S. all(l:hlist('a). implies(not(null(l)),equal(cons(hd(l),tl(l)),l))) (WOSimpC (ioid !oid{hdd simp update:s}) HNC) THENA Try (Complete Auto)

1

1. 'a:S, l:hlist('a). mt(l)  cons((hd(l)); tl(l)) = l  hlist('a)   'a:S, l:'a List. mt(l)  cons(head(l); tl(l)) = l

1 step

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