Make `inv` complete on its domain?

Today I'm running into several errors of this form:

where the failure is that `(fun p -> inv p)` and `inv` are not unifiable. I wonder if we can just make `inv` a "complete" arrow (`^->`), and somehow guide the unifier or automatically apply extensionality (probably that would be an F* improvement).

I could work around these problems, but sometimes it's not easy to find out this is what's failing.