proposition: Lemma RangeTreeBag_btraverse_bcollect : forall container keys, Permutation (List.map snd (RangeTreeBag_btraverse container.(this) keys)) (List.map snd (List.filter (fun item => Range_InRange keys (fst item)) (RangeTreeBag_bcollect container.(this)))).
proof: Proof. intros; eapply Permutation_InA_cons; [ eapply NoDupA_filter; eapply RangeTreeBag_bcollect_nodup | eapply RangeTreeBag_btraverse_nodup | ]. intros. rewrite filter_InA; [ | solve [ apply eqke_equiv ].. | ]. rewrite RangeTreeBag_btraverse_correct, RangeTreeBag_bcollect_correct. reflexivity. unfold Proper, respectful. unfold eq_key_elt, Raw.Proofs.PX.eqke. intros; eapply InRange_Proper; 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