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