Loosened some unnecessarily strong assumptions in the interface (intentional Coq eq -> "equality" of maps).