Nuprl - Proof: wellfounded functionality wrt implies 1 2

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

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:(T1

Prop). (

j:T1. (

k:T1. r1(k,j)

P(k))

P(j))

(

n:T1. P(n))
8. P : T2

Prop
9.

j:T2. (

k:T2. r2(k,j)

P(k))

P(j)

n:T1. P(n)

By:	BackThru 7 THEN Thin 7

Generated subgoal:

1 7. P : T2Prop
8. j:T2. (k:T2. r2(k,j)  P(k))  P(j)
9. j : T1
10. k:T1. r1(k,j)  P(k)
  P(j)
3 steps

About:

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