1. A : Type
2. f : AA
3. Inj(A; A; f)
4. i : 
5. 0<i
6. a1 : A
7. a2 : A
8. f{i}(a1) = f{i}(a2)
  f{i-1}(a1) = f{i-1}(a2)

By:	Compute-1 Co(f{i}(a1) * if i=0 a1 else f(f{i-1}(a1)) fi) Co= Co(f{i}(a2) * if i=0 a2 else f(f{i-1}(a2)) fi) Co A THEN SplitITE Hyp:-1

1

8. f(f{i-1}(a1)) = f(f{i-1}(a2)) 9. i  0   f{i-1}(a1) = f{i-1}(a2)

1 step

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