proposition: Lemma RangeTreeBag_bcollect_nodup : forall container, NoDupA (@eq_key _) (RangeTreeBag_bcollect container.(this)).
proof: Proof. unfold RangeTreeBag_bcollect. intro container. change (Raw.elements container) with (elements container). eapply Raw.Proofs.elements_nodup. exact (container.(is_bst)). 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