Nuprl - Proof: finite choice 1 2 1

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

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

1. A : Type
2. k :

3.

k1:

.
3. k1<k
3.

3. (

Q:(

k1

A

Prop).
3. ((

x:

k1.

y:A. Q(x;y))

(

f:(

k1

A).

x:

k1. Q(x;f(x))))
4. Q :

k

A

Prop
5.

x:

k.

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

k = 0
7. x :

(k-1)

y:A. Q(x;y)

By:	Witness5: x

Generated subgoals:

None

About:

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

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