Loukanova, R. Eta-Reduction in Type-Theory of Acyclic Recursion. ADCAIJ 2023, 12, e29199.