proposition: Lemma elements_fold_eq : forall {TValues} (m: t TValues), (elements m) = (rev (fold (fun key val acc => cons (key, val) acc) m [])).
proof: Proof. intros. rewrite fold_1. assert ((fold_left (fun (a : list (key * TValues)) (p : key * TValues) => (fst p, snd p) :: a) (elements m) []) = (fold_left (fun (a : list (key * TValues)) (p : key * TValues) => p :: a) (elements m) [])) by (f_equal; repeat (apply functional_extensionality; intros); rewrite <- surjective_pairing; reflexivity). rewrite H, fold_left_id, rev_involutive; reflexivity. 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