(37steps total) PrintForm Definitions Lemmas hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: list iso 2 2 1 1 1 1 1 1
1. 'a : S
2. f : 'a
3. n : 
  f  n'a
By: ExtWith [`f'] ['a]

Generated subgoals:

None

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

(37steps total) PrintForm Definitions Lemmas hol list 1 Sections HOLlib Doc