1. a : 
2. b : 
3. (f.<f(a-1),f>)  (a inj b)(i:b(a-1) inj {x:b| x = i })
4. (ie.ie/i,e. x.if x=a-1 i else e(x) fi)
4.  (i:b(a-1) inj {x:b| x = i })a inj b
5. f : ab
6. Inj(a; b; f)
7. a1 : a
8. a2 : a
9. if a1=a-1 f(a-1) else f(a1) fi = if a2=a-1 f(a-1) else f(a2) fi
  a1 = a2

1	9. f(a-1) = f(a2) 10. a1 = a-1 11. a2  a-1   a1 = a2	1 step
2	9. f(a1) = f(a-1) 10. a1  a-1 11. a2 = a-1   a1 = a2	1 step
3	9. f(a1) = f(a2) 10. a1  a-1 11. a2  a-1   a1 = a2	1 step

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