PLFA agda exercises
3.2.1