proposition: Lemma Permutation_Partition_App {Value}: forall (m m1 m2 : t Value), Partition m m1 m2 -> Permutation (Values m) (Values m1 ++ Values m2).
proof: Proof. unfold Partition; intros; intuition. unfold Values; rewrite <- List.map_app. eapply Permutation_InA_cons; eauto using elements_3w. eapply NoDupA_app; eauto using elements_3w, equiv_eq_key. intros; destruct x as [k v]; eapply (H0 k). apply InA_alt in H; destruct H; apply InA_alt in H2; destruct H2; intuition; unfold eq_key in *; simpl in *. destruct x; simpl in *; rewrite H3; econstructor; apply elements_2; eauto; apply In_InA; eauto using equiv_eq_key_elt. destruct x0; simpl in *; rewrite H; econstructor; apply elements_2; eauto; apply In_InA; eauto using equiv_eq_key_elt. intros; rewrite InA_app_iff by eauto using equiv_eq_key_elt; intuition. apply elements_2 in H; rewrite H1 in H; intuition; eauto using elements_1. apply elements_1; rewrite H1; eauto using elements_2. apply elements_1; rewrite H1; eauto using elements_2. 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