proposition: Corollary InvertedIndex_BagInsertEnumerate : BagInsertEnumerate InvertedIndex_RepInv InvertedIndex_benumerate InvertedIndex_binsert.
proof: Proof. unfold BagInsertEnumerate, InvertedIndex_RepInv, InvertedIndex_binsert, InvertedIndex_benumerate; intros; simpl. eapply (@MoreMValuesFacts.Permutation_InA_cons _ ((NumValues container, inserted) :: MValues.elements (ValuesMap container))). - econstructor; simpl; eauto using MValues.elements_3w. intuition. pose proof (@MValues.elements_2 _ (ValuesMap container) (NumValues container)) . eapply H3; revert H H1; clear; induction (MValues.elements (ValuesMap container)); simpl; intros; inversion H; subst; eauto. destruct a as [k v]; eexists v; eapply H1; econstructor; simpl. econstructor; simpl; eauto. - eauto using MValues.elements_3w. - intros; rewrite <- !elements_mapsto_iff, add_mapsto_iff; intuition; subst. + econstructor; reflexivity. + econstructor 2; rewrite <- elements_mapsto_iff; eauto. + inversion H0; subst; [left | right]; intuition. destruct H4; simpl in *; subst; eauto. destruct H4; simpl in *; subst; eauto. rewrite <- elements_mapsto_iff in H4; subst. eapply H2; eauto; eexists; eauto. rewrite <- elements_mapsto_iff in H4; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.Peano_dec Coq.Structures.OrdersEx Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListInclusion