1. A : Type
2. x : A
3. f : AA
4. i : 
5. i1:. i1<i  (j,k:. k = i1+j  f{i1}(f{j}(x)) = f{k}(x))
6. j : 
7. k : 
8. k = i+j
9. i = 0
  f{i}(f{j}(x)) = f{k}(x)

By:	Rewrite by Thm*  f:(AA), i:, x:A. f{i}(x) = f(f{i-1}(x))

1

f(f{i-1}(f{j}(x))) = f(f{k-1}(x))

2 steps

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