proposition: Lemma Values_fold_Proper : forall {A}, Proper (E.eq ==> eq ==> Permutation (A:=A) ==> Permutation (A:=A)) (fun (_ : key) (val : A) (acc : list A) => val :: acc).
proof: Proof. unfold Proper, respectful; intros. subst; eauto. 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