1. a : 
2. b : 
3. (f.<f(a-1),f>)  (a inj b)(i:b(a-1) inj {x:b| x = i })
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

By:	BackThru:  Thm*  a:, b:, j:b, f:((a-1) inj {x:b| x = j }). Thm*  (i.if i=a-1 j else f(i) fi)  a inj b

None

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