Nuprl - well_fnd LEMMAs for wellfounded_functionality_wrt

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

Theorem	Name
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)))	[wellfounded_functionality_wrt_iff]
cites the following:
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))	[wellfounded_functionality_wrt_implies]

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