A:Type, r:(AAProp), B:Type, f:(BA).
  WellFnd{i}(A;x,y.r(x,y))  WellFnd{i}(B;x,y.r(f(x),f(y)))

By:	Lemma Thm* r:(TTProp), S:Type, f:(ST). Thm* WellFnd{i}(T;x,y.r(x,y))  WellFnd{i}(S;x,y.r(f(x),f(y)))

None

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