D. Baelde, “Abella: A System for Reasoning about Relational Specifications”, JFR, vol. 7, no. 2, pp. 1–89, Jan. 2014.