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

By:	FwdThru:  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))) on [ Thm* WellFnd{i}(;x,y.x<y) ] Using:[S:= {n...} | f(x):= x-n]

1

2. WellFnd{i}({n...};x,y.x-n<y-n)   WellFnd{i}({n...};x,y.x<y)

1 step

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