Nuprl - Proof: decidable-exists-finite 1 1

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

1. T : Type
2. P : T

Prop
3.

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

5. f :

T
6. Surj(

n; T; f)

(

x:T. P(x))

(

n. P(f(i)))

By:	Unfold `surject` -1 THEN ExRepD

Generated subgoals:

1 6. b:T. a:n. f(a) = b
7. x : T
8. P(x)
i:n. P(f(i))
2 steps

2 6. b:T. a:n. f(a) = b
7. i : n
8. P(f(i))
x:T. P(x)
1 step

About:

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

1	6. b:T. a:n. f(a) = b 7. x : T 8. P(x) i:n. P(f(i))	2 steps
2	6. b:T. a:n. f(a) = b 7. i : n 8. P(f(i)) x:T. P(x)	1 step