(11steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: surjection type surjection 1 1 1 1 1
1. A : Type
2. B : Type
3. f : AB
4. Surj(A; B; f)
5. a : 
6. s : aA
7. Surj(a; A; s)
8. B Discrete
9. f o s  aB
10. Surj(a; B; f o s)
11. e : BB
12. x,y:B. (x e y)  x = y
13. b : B
  i:a. ((f o s)(i)) e b
By: Rewrite by Hyp:12

Generated subgoal:

1   i:a. (f o s)(i) = b
1 step

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

(11steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc