Some background on optimal beta reduction: Levy, Lamping.\xa0 The main problem to overcome is duplicating a lambda abstraction that is used in two different places in your term.\xa0 The solution is to try to duplicate it incrementally.