proposition: Lemma fold_spec_right m {A}(i:A)(f : key -> elt -> A -> A) : fold f m i = List.fold_right (uncurry f) i (rev (bindings m)).
proof: Proof. rewrite fold_1. symmetry. apply fold_left_rev_right. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)