proposition: Lemma IndexedBag_BagFindCorrect : BagFindCorrect IndexedBag_RepInv IndexedBag_bfind Matcher IndexedBag_benumerate.
proof: Proof. unfold BagFindCorrect, IndexedBag_RepInv, IndexedBag_bfind, IndexedBag_benumerate. intros [ibag pool] st [repi _]; simpl in *. eapply perm_trans; [ | eapply IndexesToItems_perm; symmetry; eapply ibfind_correct ]; eauto. induction (ibenumerate ibag); eauto; simpl. unfold IBagMatcher in *; destruct (pget pool a) eqn: eq; simpl in *. - destruct (Matcher st t); eauto. simpl. rewrite eq. eapply perm_skip; eauto. - 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