proposition: Lemma 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.
proof: Proof. intros A f Hf dom m. unfold for_all, find. rewrite fold_spec. change (∀ (x : key) (v : A), S.find x m = Some v → f x v = true) with (∀ (x : key) (v : A), S.find (fst (x, v)) m = Some (snd (x, v)) → f x v = true). setoid_rewrite <- elements_spec. rewrite for_all_spec_aux; tauto || eassumption. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface