Nuprl - Proof: dep finite choice 1 2 1

(25steps total) Remark PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: dep finite choice 1 2 1

1. k :

2.

k1:

.
2. k1<k
2.

2. (

B:(

k1

Type), Q:(x:

k1

B(x)

Prop).
2. ((

x:

k1.

y:B(x). Q(x;y))

(

f:(x:

k1

B(x)).

x:

k1. Q(x;f(x))))
3. B :

k

Type
4. Q : x:

k

B(x)

Prop
5.

x:

k.

y:B(x). Q(x;y)
6.

k = 0
7. x :

(k-1)

y:B(x). Q(x;y)

By:	BackThru: Hyp:5

Generated subgoals:

None

About:

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

(25steps total) Remark PrintForm Definitions DiscreteMath Sections DiscrMathExt Doc