Nuprl - Proof: finite choice 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

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)

f:(

k

A).

x:

k. Q(x;f(x))

By:	Decide: k = 0

Generated subgoals:

1 6. k = 0
  f:(kA). x:k. Q(x;f(x))
1 step

2 6. k = 0
  f:(kA). x:k. Q(x;f(x))
12 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