proposition: Lemma fold_Equiv_ext : forall (f : E.t -> A -> B -> B) (f_m : Proper (E.eq ==> eq ==> eqB ==> eqB) f) (hf : transpose_neqkey eqB f) f', (forall k k', E.eq k k' -> forall x x', eq x x' -> forall b b', eqB b b' -> eqB (f k x b) (f' k' x' b')) -> forall m m', Equiv eq m m' -> forall b b', eqB b b' -> eqB (fold f m b) (fold f' m' b').
proof: Proof. intros f f_m hf f' ff' m m' mm' b b' bb'. rewrite !fold_1. set (F := fun a (p:key*A) => f (fst p) (snd p) a). set (F' := fun a (p:key*A) => f' (fst p) (snd p) a). trans (fold_left F (elements m') b'). unfold F. rewrite <- !fold_1. apply fold_Equiv; auto||refl. apply fold_left_m_ext with (eqB:=@eq_key_elt A); try refl. intros a a' aa' [k x] [k' x'] e. inversion e. unfold F, F'. simpl in *. subst x'. apply ff'; auto||refl. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)