fact: Parameter exists_spec : forall A f, Proper (X.eq ==> Logic.eq ==> Logic.eq) f -> forall dom (m : t A dom), exists_ f m = true <-> exists x v, find x m = Some v ∧ f x v = true.
imports: Utf8 Orders Coqlib DepMapInterface