T:Type, R:(TTType). SWellFounded(R(x,y))  WellFnd{i}(T;x,y.R(x,y))

1

1. T : Type 2. R : TTType 3. f : T 4. x,y:T. R(x,y)  f(x)<f(y) 5. P : TProp 6. j:T. (k:T. R(k,j)  P(k))  P(j)   n:T. P(n)

4 steps

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