proposition: Corollary constant_OK : forall A dom v, OK dom (Dom.fold (fun x m => S.add x v m) dom (S.empty A)).
proof: Proof. intros * ?. rewrite Dom.fold_spec, <- Dom.elements_spec1, constant_OK_aux. intuition. destruct H0 as [? Hin]. elim (S.empty_1 Hin). Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface