b'
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.