Хотелось бы узнать, какого рода враньё.
Я предполагаю, что оно может возникнуть по 4 причинам:
1) баг в alphaEq, который некоторые эквивалентные термы не считает таковыми
2) баг в reduce, приводящий к циклу длиной более 1 либо к "как это будет редукция наоборот"
3) терм, описывающий рекурсивное выражение, который при редукции не сокращается, а раскрывается всё больше и больше
4) подлинно рекурсивный терм, вида let t = App t t in t - для которого синтаксическое дерево анализировать бесполезно, нужна редукция на графе