proposition: Lemma FMap_Insert_fold_add_map_eq {Value} : forall (f : Value -> Value) (bag : t Value), Equal (fold (fun k bag'' r' => add k (f bag'') r') bag (empty _)) (map f bag).
proof: Proof. unfold Equal. intros; case_eq (find y (fold (fun (k : key) (bag'' : Value) (r' : t Value) => add k (f bag'') r') bag (empty Value))); intros; case_eq (find y (map f bag)); intros; eauto. - apply find_2 in H; apply find_2 in H0. apply FMap_Insert_fold_add_MapsTo in H; destruct H. exfalso; apply empty_mapsto_iff in H; eauto. apply map_mapsto_iff in H0; destruct H0 as [a [eq_a MapsTo_y]]; subst. generalize (elements_3w bag); apply elements_1 in MapsTo_y; induction MapsTo_y; intros. + inversion H1; subst; destruct H0; simpl in *; subst. inversion H; subst; [destruct H3; simpl in *; subst; eauto | exfalso; apply H4; revert H0 H3; clear; induction l; intros; inversion H3; subst; unfold eq_key in *]. destruct H1; simpl in *; subst; constructor; eauto. constructor 2; eauto. + inversion H0; subst; eapply IHMapsTo_y; eauto. inversion H; subst; eauto. destruct H2; simpl in *; subst. exfalso; apply H3; revert H1 MapsTo_y; clear; induction l; intros; inversion MapsTo_y; subst; unfold eq_key in *. destruct H0; simpl in *; subst; constructor; eauto. constructor 2; eauto. - apply find_2 in H; apply FMap_Insert_fold_add_MapsTo in H; destruct H. exfalso; apply empty_mapsto_iff in H; eauto. apply InA_Map in H; destruct H as [[k v'] [eq_k In_k]]; simpl in *. destruct eq_k; simpl in *; rewrite H in H0. apply not_find_in_iff in H0; exfalso; eapply H0. apply map_in_iff; exists v'; apply elements_2. apply InA_alt; eexists; repeat split; eauto. - apply find_2 in H0; apply not_find_in_iff in H. apply map_mapsto_iff in H0; destruct H0 as [k [k_eq MapsTo_k]]; subst. exfalso; apply H. econstructor 1 with (x := f k); apply FMap_fold_add_MapsTo_In. apply elements_1 in MapsTo_k; revert MapsTo_k; clear; intro; induction MapsTo_k; simpl. repeat constructor; destruct H; simpl in *; subst; eauto. constructor 2; eauto. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances