Nuprl - Proof: finite choice 1 2

(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. 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

f:(

k

A).

x:

k. Q(x;f(x))

By:	Inst: Hyp:3 Using:[k-1 \| Q]

Generated subgoals:

1 7. x : (k-1)
y:A. Q(x;y)
1 step

2 7. f:((k-1)A). x:(k-1). Q(x;f(x))
f:(kA). x:k. Q(x;f(x))
10 steps

About:

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

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