proposition: Corollary from_elements_OK : forall A l, OK (fold_left (fun acc xv => Dom.add (fst xv) acc) l Dom.empty) (fold_left (fun acc xv => S.add (fst xv) (snd xv) acc) l (S.empty A)).
proof: Proof. intros. change Dom.empty with (domain (@empty A)). change (S.empty A) with (proj1_sig (@empty A)). apply pre_from_elements_OK. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface