proposition: Corollary RangeTreeBag_btraverse_closed : forall container searchkey key bag, InA (@eq_key_elt _) (key, bag) (RangeTreeBag_btraverse container.(this) searchkey) -> MapsTo key bag container.
proof: Proof. intros container searchkey key' bag' H. rewrite RangeTreeBag_btraverse_correct in H. tauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts