(8steps total) Remark PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub surj least preimage total gen 1
1. B : Type
2. e : BB
3. IsEqFun(B;e)
4. a : 
5. f : a onto B
6. y : B
  (least x:. (f(x)) e y)  a
By: Analyze-2

Generated subgoal:

1 5. f : aB
6. Surj(a; B; f)
7. y : B
  (least x:. (f(x)) e y)  a
6 steps

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

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