Nuprl - Proof: wellfounded functionality wrt implies 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: wellfounded functionality wrt implies 1 2 1 1

1. T1 : Type
2. T2 : Type
3. r1 : T1

Prop
4. r2 : T2

Prop
5. T1 = T2
6.

x,y:T1. r1(x,y)

r2(x,y)
7. P : T2

Prop
8. j : T1
9.

k:T1. r1(k,j)

P(k)
10. k : T2
11. r2(k,j)

P(k)

By:	BackThru 9 THEN Thin 9

Generated subgoal:

1 9. k : T2
10. r2(k,j)
r1(k,j)
1 step

About:

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