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:	Rewrite by i = 0   ... THEN Rewrite by k = 0   ... THENA (Rewrite8 by i = 0 ...)

1

f{0}{j}(x) = f{0}(x)

2 steps

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