proposition: Lemma fold_4 : forall s s' x (A : Type) (eqA : A -> A -> Prop) (st : Equivalence eqA) (i : A) (f : elt -> A -> A), Proper (E.eq==>eqA==>eqA) f -> Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)).
proof: Proof. intros. rewrite !fold_spec. change (eqA (fold_left (flip f) (elements s') i) (fold_left (flip f) (x::elements s) i)). unfold flip; rewrite <-!fold_left_rev_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. apply elements_Add_Below; auto. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide