proposition: Lemma fold_alist_alt (map: alist) : forall acc: T, fold_alist acc map = fold_alist' acc map.
proof: Proof. induction map; intuition. simpl. rewrite IHmap. reflexivity. Qed.
imports: Coq.Classes.RelationClasses Coq.Lists.List ExtLib.Core.RelDec ExtLib.Tactics.Consider ExtLib.Structures.Maps ExtLib.Structures.Monad ExtLib.Structures.Reducible ExtLib.Structures.Functor Coq(Basics) ExtLib(Extras OptionMonad)