PLFA agda exercises
3.10