PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sized mset wf2
  a,k,x:, y:. a {k} {x..y}  Type
By: Def of <nat> {<nat>} <Nat subtype>

Generated subgoals:

None

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

PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc