proposition: Lemma IndexedBag_BagCountCorrect : BagCountCorrect IndexedBag_RepInv IndexedBag_bcount IndexedBag_bfind.
proof: Proof. unfold BagCountCorrect, IndexedBag_RepInv, IndexedBag_bcount, IndexedBag_bfind. intros [ibag pool] st [repi repp]; simpl in *. rewrite <- ibcount_correct; eauto. specialize (fun i => proj1 (repp i)); clear repp; intro repp. assert (forall i, List.In i (ibfind ibag st) -> pget pool i <> None). intros i asmp. apply repp. eapply List.filter_In. eapply Permutation_in. eapply ibfind_correct; eauto. eauto. induction (ibfind ibag st); eauto. destruct (InList_ind_helper H) as [H_h H_t]; clear H. simpl; destruct (pget pool a); try congruence. simpl. f_equal. apply IHl. eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.Structures.OrderedTypeEx