PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: length nil 2
  'a:S, l:'a List. ||l|| = 0    l = nil
By: RewriteOfThm
Thm* 'a:S. all(l:hlist('a). equal(equal(length(l),0),equal(l,nil)))
(SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

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

PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc