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
9. a1 :
(a-1)
10.
(a-1)
if a1=a-1 i else e(a1) fi {x:b| x = i }
