PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list induct
  'a:S, P:(('a List)).
  P(nil) & (t:'a List. P(t)  (h:'a. P(cons(h; t))))  (l:'a List. P(l))
By: RewriteOfThm Thm: hlist induct (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

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

PrintForm Definitions Lemmas hol list 2 Sections HOLlib Doc