Make inverse rewrite laws for pseudofunctor
Add [unique pose proof] and [unique pose] to Tactics.v
Add some typeclass resolution hints for apply being stupid

[apply] doesn't know that, e.g., the identity functor applied to x is
x, nor vice-versa.  And because it infers arguments in the "wrong"
order, it errors before it has a chance to pick up that information.
So we need to help it along a little.
Add some convenience lemmas for removing isomorphisms
Mostly finish lax comma categories
Fix core
Remove useless includes