Make `compose` a notation rather than a definition

This makes life a lot easier; we don't have to be constantly unfolding it, and we can avoid `Local Arguments compose /.` and `simpl rewrite` in lots of places.
There should not be a `try` here; the `repeat match` takes care of that already.  Furthermore, having the `try` means that any cases below this one will never get triggered; although it doesn't matter here, it's bad practice.

In any case, I'm also not entirely happy with this one (I'd prefer a pattern to identity the right goal), but this gripe (about wanting a pattern) is very minor.