1. T : Type
2. r : TTProp
3. S : Type
4. f : ST
5. WellFnd{i}(T;x,y.r(x,y))
  WellFnd{i}(S;x,y.r(f(x),f(y)))

1

P:(SProp). (j:S. (k:S. r(f(k),f(j))  P(k))  P(j))  (n:S. P(n))

30 steps

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