Blanchette, J., & Vukmirović, P. (2023). SAT-Inspired Higher-Order Eliminations. Logical Methods in Computer Science, 19(2): 9, pp. 1-23. doi:10.46298/lmcs-19(2:9)2023.