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
  f{i}{j}(x) = f{k}(x)

By:	Rewrite by j = 0   ...a THEN Rewrite by k = 0   ...a THENA (Rewrite8 by j = 0 ...)

1

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

1 step

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