Nuprl - Proof: inv image ind a 1

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

1. T : Type
2. r : T

Prop
3. S : Type
4. f : S

T
5. WellFnd{i}(T;x,y.r(x,y))

WellFnd{i}(S;x,y.r(f(x),f(y)))

By:	RepUnfolds [`wellfounded`;`guard`] 0 THEN RepD

Generated subgoal:

1 6. P : SProp
7. j:S. (k:S. r(f(k),f(j)) P(k)) P(j)
8. n : S
P(n)
5 steps

About:

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