1 | 7. a:Alph*. a E a 8. a,b:Alph*. (a E b)  (b E a) 9. a,b,c:Alph*. (a E b)  (b E c)  (a E c) 10. x,y:Alph*. Dec(x E y) 11. a: n* map(f;a) E map(f;a) |
2 | 7. a:Alph*. a E a 8. a,b:Alph*. (a E b)  (b E a) 9. a,b,c:Alph*. (a E b)  (b E c)  (a E c) 10. x,y:Alph*. Dec(x E y) 11. a: n* 12. b: n* 13. map(f;a) E map(f;b) map(f;b) E map(f;a) |
3 | 7. a:Alph*. a E a 8. a,b:Alph*. (a E b)  (b E a) 9. a,b,c:Alph*. (a E b)  (b E c)  (a E c) 10. x,y:Alph*. Dec(x E y) 11. a: n* 12. b: n* 13. c: n* 14. map(f;a) E map(f;b) 15. map(f;b) E map(f;c) map(f;a) E map(f;c) |