proposition: Lemma negb_KeyBasedPartitioningFunction_Proper : forall BagType reference, Proper (E.eq ==> eq ==> eq) (fun k e => negb (KeyBasedPartitioningFunction BagType reference k e)).
proof: Proof. intros; unfold KeyBasedPartitioningFunction, Proper, respectful; intros x y E_eq **; subst; destruct (F.eq_dec x _), (F.eq_dec y _); rewrite E_eq in *; intuition. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances