proposition: Lemma fold_equiv {A} m (f : key -> elt -> A -> A) (a : A) : fold f m a = fold' f m a.
proof: Proof. unfold fold', bindings. now rewrite fold_equiv_aux. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)