1. T : Type
2. r : TTProp
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
6. P : SProp
7. j:S. (k:S. r(f(k),f(j))  P(k))  P(j)
8. n : S
  P(n)

By:	Assert (x:T, y:S. f(y) = x  P(y)) THEN IfLabL [`assertion`,(Analyze 0);`main`,(InstHyp [f(n);n] -1)]

1

9. x : T   y:S. f(y) = x  P(y)

4 steps

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