Perform substitution in a binder's input type
Add beta reduction for applications