- hide the closure variable
- split t_app_beta into t_func_app_beta, which returns terms,
  and t_pred_app_beta which returns formulas

Also:
- check for non-recursivity in t_open_lambda
- implement t_is_lambda via t_open_lambda (less efficient,
  but the correct code without opening would be horrendous)
- drop t_app_lambda, subsumed by t_[func|pred]_app_beta
- support nested lambdas in t_[func|pred]_app_beta