some progress towards making proof of decidability of alpha equality be  transparent exactly upto the decision part; so that it can compute efficiently.
better example of a term in LetrecEx.