Nuprl - Proof: inv image ind tp 1 1 1 1 1 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv image ind tp 1 1 1 1 1 1 2 1 1

1. T : Type
2. r : T

Prop
3. S : Type
4. f : S

T
5. WellFnd{i}(T;x,y.r(x,y))
6. P : S

Prop
7.

j:S. (

k:S. r(f(k),f(j))

P(k))

P(j)
8. j : T
9.

k:T. r(k,j)

(

n:S. f(n) = k

P(n))
10. n : S
11. f(n) = j

nn:S. r(f(nn),f(n))

P(nn)

By:	(Analyze 0) THEN (Analyze 0)

Generated subgoals:

1 12. nn : S
13. r(f(nn),f(n))
  P(nn)
7 steps

2 12. nn : S
  r(f(nn),f(n))  Prop
1 step

3   S  Type
1 step

About:

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