Nuprl - Proof: decidable-exists-finite 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable-exists-finite 1 1 1 1

1. T : Type
2. P : T

Prop
3.

x:T. Dec(P(x))
4. n :

5. f :

T
6.

b:T.

n. f(a) = b
7. x : T
8. P(x)
9. a :

n
10. f(a) = x

P(f(a))

By:	HypSubst -1 0

Generated subgoals:

None

About:

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