i:, j:{i...}. WellFnd{u}({i..j};x,y.x<y)

By:	Auto THEN FwdThru:  Thm* r:(AAProp), B:Type, f:(BA). Thm* WellFnd{i}(A;x,y.r(x,y))  WellFnd{i}(B;x,y.r(f(x),f(y))) on [ WellFnd{u}({i...};x,y.x<y) ] Using:[B:= {i..j} | f(x):= x]

1

1. i :  2. {i...}   WellFnd{u}({i...};x,y.x<y)

1 step

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