(15steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Principle of finite choice. The function can be constructed explicitly without appeal to the Axiom of Choice.

At: finite choice

  A:Type, k:, Q:(kAProp).
  (x:k. y:A. Q(x;y))  (f:(kA). x:k. Q(x;f(x)))
By: Analyze THEN CompNatInd Concl

Generated subgoal:

1 1. A : Type
2. k : 
3. k1:. 
3. k1<k
3. 
3. (Q:(k1AProp). 
3. ((x:k1. y:A. Q(x;y))  (f:(k1A). x:k1. Q(x;f(x))))
4. Q : kAProp
5. x:k. y:A. Q(x;y)
  f:(kA). x:k. Q(x;f(x))
14 steps

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

(15steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc