proposition: Lemma fold_spec : forall A B (f : key -> A -> B -> B) dom (m : t A dom) (i : B), fold f m i = List.fold_left (fun acc xv => f (fst xv) (snd xv) acc) (elements m) i.
proof: Proof. intros. unfold fold, elements. rewrite S.fold_1. reflexivity. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface