proposition: Lemma foldkeys_Proper : Proper (Eqdom==>eqA==>eqA) foldkeys.
proof: Proof. Proof using st Hf Hf'. intros m1 m2 Hm i j Hi. unfold foldkeys. rewrite 2 fold_spec_right. assert (NoDupA eqk (rev (bindings m1))). { apply NoDupA_rev; auto with *. apply bindings_spec2w. } assert (NoDupA eqk (rev (bindings m2))). { apply NoDupA_rev; auto with *. apply bindings_spec2w. } apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqk) ; auto with *. - intros (k1,e1) (k2,e2) Hk a1 a2 Ha; simpl in *. now apply Hf. - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto with map. compute. simpl in *. red in Hf'. eapply (@Hf' a a0); eauto. eapply Hf; eauto; easy. eapply Hf; eauto; easy. - rewrite <- NoDupA_altdef; auto. - intros (k,e). rewrite 2 InA_rev. specialize (Hm k). now rewrite <- !in_bindings_iff'. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)