in alpha-equivalence checking of formulas, protect against type errors
better implementation of beta reduction in Lambda, with a separate
function to apply a lambda term to already-reduced arguments