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
  InvFuns(a inj b;i:b(a-1) inj {x:b| x = i }
  InvFuns;f.<f(a-1),f>;ie.ie/i,e. x.if x=a-1 i else e(x) fi)

1	5. f : ab 6. Inj(a; b; f)   (x.if x=a-1 f(a-1) else f(x) fi) = f  a inj b	8 steps
2	5. i : b 6. e : (a-1){x:b| x = i } 7. Inj((a-1); {x:b| x = i }; e)   <if a-1=a-1 i else e(a-1) fi,x.if x=a-1 i else e(x) fi>   =   <i,e>    i:b(a-1) inj {x:b| x = i }	13 steps

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