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. i : b
6. e : (a-1){x:b| x = i }
7. Inj((a-1); {x:b| x = i }; e)
8. a-1 = a-1
  Inj((a-1); {x:b| x = i }; x.if x=a-1 i else e(x) fi)

By:	Guarding if <bool> <*> else <else> fi (Def THEN Reduce Concl)

1	9. a1 : (a-1) 10. a2 : (a-1) 11. if a1=a-1 i else e(a1) fi = if a2=a-1 i else e(a2) fi   a1 = a2	2 steps
2	9. a1 : (a-1) 10. (a-1)   if a1=a-1 i else e(a1) fi  {x:b| x = i }	1 step
3	9. (a-1) 10. a2 : (a-1)   if a2=a-1 i else e(a2) fi  {x:b| x = i }	1 step

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