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

At: dep finite choice

  k:, B:(kType), Q:(x:kB(x)Prop).
  (x:k. y:B(x). Q(x;y))  (f:(x:kB(x)). x:k. Q(x;f(x)))
By: CompNatInd Concl

Generated subgoal:

1 1. k : 
2. k1:. 
2. k1<k
2. 
2. (B:(k1Type), Q:(x:k1B(x)Prop).
2. ((x:k1. y:B(x). Q(x;y))  (f:(x:k1B(x)). x:k1. Q(x;f(x))))
3. B : kType
4. Q : x:kB(x)Prop
5. x:k. y:B(x). Q(x;y)
  f:(x:kB(x)). x:k. Q(x;f(x))
24 steps

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

(25steps total) PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc