proposition: Lemma fold_right_add : forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)).
proof: Proof. intros s' s x **; apply (@fold_right_equivlistA s' (x::s)); auto. Qed.
imports: List Sorted Setoid Basics Morphisms