PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: boolsize wf
  a:. size(a)  (a)
By: Def of size(<nat>)

Generated subgoals:

None

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

PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc