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 eq nil
  'a:S, P:(('a List)). (l:'a List. ||l|| = 0    P(l))  P(nil)
By: RewriteOfThm
Thm* 'a:S. 
Thm* all
Thm* (P:hlist('a)  hbool. equal
Thm* (P:hlist('a)  hbool. (all
Thm* (P:hlist('a)  hbool. ((l:hlist('a). implies(equal(length(l),0),P(l)))
Thm* (P:hlist('a)  hbool. ,P(nil)))
(SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

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

PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc