Make inv complete on its domain?

[mtzguido]

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.