1. a : 
2. b : 
  (a inj b) ~ (i:b(a-1) inj {x:b| x = i })

By:	Witness: Wif.<f(a-1),f> Wiwith type (a inj b)(i:b(a-1) inj {x:b| x = i }) THEN Witness: Wiie.ie/i,e. x.if x=a-1 i else e(x) fi Wiwith type (i:b(a-1) inj {x:b| x = i })a inj b

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

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