Nuprl - Proof: wellfounded functionality wrt iff 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: wellfounded functionality wrt iff 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)

WellFnd{i}(T1;x,y.r1(x,y))

WellFnd{i}(T2;x,y.r2(x,y))

By:	BackThru Thm* r1:(T1T1Prop), r2:(T2T2Prop). Thm* T1 = T2 Thm* Thm* (x,y:T1. r1(x,y) r2(x,y)) Thm* Thm* WellFnd{i}(T1;x,y.r1(x,y)) WellFnd{i}(T2;x,y.r2(x,y))

Generated subgoals:

1 T2 = T1
Trivial

2 x,y:T2. r2(x,y) r1(x,y)
1 step

About:

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