Loosened some unnecessarily strong assumptions in the interface

It doesn't make sense to make something "Proper" wrt Coq's intensional equality, since — by definition of the latter — *everything* is. What you want here is the "equality" you define on maps. This has one extra implicit argument, and since it's not maximally inserted, it has to be given (another way would be to use (eq (A := A)) instead of (@eq _), same thing.

— Filip