proposition: Lemma fold_Equal2 : forall m1 m2 i j, Equal m1 m2 -> eqA i j -> eqA (fold f m1 i) (fold f m2 j).
proof: Proof. intros. rewrite 2 fold_spec_right. assert (NoDupA eqk (rev (elements m1))) by auto with map typeclass_instances. assert (NoDupA eqk (rev (elements m2))) by auto with map typeclass_instances. apply fold_right_equivlistA_restr2 with (R:=complement eqk)(eqA:=eqke). 1:auto with typeclass_instances. 1, 10: auto. 2: auto with crelations. 4, 5: auto with map. - intros (k1,e1) (k2,e2) (Hk,He) a1 a2 Ha; simpl in *; apply Comp; auto. - unfold complement, eq_key, eq_key_elt; repeat red. intuition eauto. - intros (k,e) (k',e') z z' h h'; unfold eq_key, uncurry;simpl; auto. rewrite h'. auto. - rewrite <- NoDupA_altdef; auto. - intros (k,e). rewrite 2 InA_rev, <- 2 elements_mapsto_iff, 2 find_mapsto_iff, H. auto with crelations. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface