1. A : Type
2. x : A
3. f : AA
4. i : 
5. j : 
6. j1:. j1<j  (k:. k = ij1  f{i}{j1}(x) = f{k}(x))
7. k : 
8. k = ij
9. j = 0
10. i = 0
  f{i}{j}(x) = f{k}(x)

By:	Inst: Thm*  a,b:, n:. ab  nanb Using:[n:= i | 1 | j] ...a

1

11. i1ij   f{i}{j}(x) = f{k}(x)

5 steps

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