proposition: Lemma IndexedBag_BagFindCorrect : BagFindCorrect IndexedBag_RepInv IndexedBag_bfind IndexedBag_bfind_matcher IndexedBag_benumerate.
proof: Proof. intros; hnf. destruct search_term as (option_key, search_term). destruct option_key as [ key | ]. unfold IndexedBag_benumerate, IndexedBag_bfind, IndexedBag_bfind_matcher. unfold IndexedBag_RepInv; intros. rewrite filter_and. rewrite flatten_filter. simpl. rewrite consist. case_eq (M.find key container); intros. apply bfind_correct. eapply containerCorrect; rewrite find_mapsto_iff; eauto. eauto. unfold IndexedBag_RepInv; eauto. simpl. unfold IndexedBag_benumerate, IndexedBag_bfind_matcher, IndexedBag_RepInv, IndexedBag_bfind. rewrite flatten_filter; intros. pose proof (alt_IndexedBag_RepInv _ containerCorrect) as containerCorrect'. revert TBagCorrect containerCorrect'; clear. unfold Values; induction (elements container); simpl; eauto; intros. apply Permutation_app. apply (bfind_correct _). destruct a; eapply containerCorrect'; repeat constructor; eauto. rewrite IHl; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Arith.PeanoNat Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts