proposition: Lemma fold_equiv_aux {A} m (f : key -> elt -> A -> A) (a : A) acc : L.fold f (bindings_aux acc m) a = L.fold f acc (fold f m a).
proof: Proof. revert a acc. induction m; simpl; trivial. intros. rewrite IHm1. simpl. apply IHm2. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)