proposition: Lemma InA_InRange_bcollect_btraverse : forall k v keys container, InA (eq_key_elt (elt:=BagType)) (k, v) (List.filter (fun x : TKey * BagType => Range_InRange keys (fst x)) (RangeTreeBag_bcollect container.(this))) <-> InA (eq_key_elt (elt:=BagType)) (k, v) (List.filter (fun x : TKey * BagType => Range_InRange keys (fst x)) (RangeTreeBag_btraverse container.(this) keys)).
proof: Proof. intros k v keys container. rewrite !filter_InA; try solve [ apply eqke_equiv ]. - rewrite RangeTreeBag_btraverse_correct, RangeTreeBag_bcollect_correct in *. intuition. - unfold Proper, respectful; intros; apply InRange_Proper. unfold eq_key_elt, Raw.Proofs.PX.eqke in *; intuition. - unfold Proper, respectful; intros; apply InRange_Proper. unfold eq_key_elt, Raw.Proofs.PX.eqke in *; intuition. 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