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):= j+i-x]

1	1. i :  2. {i...}   WellFnd{u}({i...};x,y.x<y)	1 step
2	1. i :  2. j : {i...} 3. WellFnd{u}({i..j};x,y.j+i-x<j+i-y)   WellFnd{u}({i..j};x,y.x>y)	1 step

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html