'a:S, l:'a List. l = nil  (t:'a List, h:'a. l = cons(h; t))

By:	RewriteOfThm 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)))))) (SimpsetC [`hol_to_nuprl`;`bequal`])

None

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