Bugfix

This resolves #1, as well as another issue I noticed where the congruences for `app` and `lam` were insufficiently constrained.