proposition: Lemma fold_empty : forall {TValue TAcc} f (default: TAcc), fold f (empty TValue) default = default.
proof: Proof. intros; apply fold_Empty; eauto using empty_1. 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