proposition: Corollary Permutation_partition {Value}: forall f (m : t Value), (Proper (E.eq ==> eq ==> eq) f) -> Permutation (Values m) (Values (fst (partition f m)) ++ Values (snd (partition f m))).
proof: Proof. intros; eauto using Permutation_Partition_App, partition_Partition_simple. 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