Backhouse, R. C., Guttmann, W., & Winter, M. (2024). An example of goal-directed, calculational proof. Journal of Functional Programming, 34, Article e13. https://doi.org/10.1017/s095679682400011x