Eta-Reduction in Type-Theory of Acyclic Recursion

+