1. a : 
2. b : 
3. (f.<f(a-1),f>)  (a inj b)(i:b(a-1) inj {x:b| x = i })
  (ie.ie/i,e. x.if x=a-1 i else e(x) fi)
   (i:b(a-1) inj {x:b| x = i })a inj b

1

4. i:b(a-1) inj {x:b| x = i } 5. i : b 6. e : (a-1) inj {x:b| x = i }   (x.if x=a-1 i else e(x) fi)  a inj b

1 step

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