(10steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: least characterized2 1
1. p : {p:()| i:. p(i) }
  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }
By: Analyze-1 THEN Analyze-1

Generated subgoal:

1 1. p : 
2. i : 
3. p(i)
  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }
8 steps

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

(10steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc