proposition: Lemma KeyFilter_beq : forall beq, (forall x y, reflect (E.eq x y) (beq x y)) -> (forall key (item: TItem), KeyFilter key item = beq (projection item) key).
proof: Proof. intros beq spec key item. specialize (spec (projection item) key). unfold KeyFilter. destruct spec as [ is_eq | neq ]; destruct (F.eq_dec _ _); intuition. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Arith.PeanoNat Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts