Nuprl - Proof: inv image ind a 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv image ind a 1 1 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. S
9. j : T
10.

k:T. r(k,j)

(

y:S. f(y) = k

P(y))
11. y : S
12. f(y) = j

P(y)

By:	Assert (y':S. r(f(y'),f(y)) P(y')) THEN IfLabL [`main`,(OnHyps [12;10;9;8] Thin);`assertion`,RepD]

Generated subgoals:

1 13. y' : S
14. r(f(y'),f(y))
  P(y')
1 step

2 8. y : S
9. y':S. r(f(y'),f(y))  P(y')
  P(y)
1 step

About:

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

1	13. y' : S 14. r(f(y'),f(y)) P(y')	1 step
2	8. y : S 9. y':S. r(f(y'),f(y)) P(y') P(y)	1 step