1. n : 
2. WellFnd{i}({-n...};x,y.x<y)
  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 [ Hyp:-1 ] Using:[S:= {...n} | f(x):= -x]

1

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

1 step

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