proposition: Lemma values_add_not_in {A : Type} : forall (m: t A), forall k v, ~ In k m -> Permutation (Values (add k v m)) (v :: Values m).
proof: Proof. intros. unfold Values. rewrite elements_fold_eq. rewrite map_rev. rewrite map_fold; simpl. etransitivity. symmetry. etransitivity; [ | apply Permutation_rev]. symmetry. apply (fold_add (elt := A) (eqA := @Permutation A )); eauto. apply Permutation_Equivalence. unfold Proper, respectful; intros; simpl; subst; apply Permutation_cons; try reflexivity; assumption. unfold transpose_neqkey; intros; simpl; constructor. rewrite fold_1. rewrite fold_left_map. econstructor. rewrite Permutation_rev. rewrite map_rev. rewrite 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