proposition: Lemma fold_right_commutes_restr : forall s1 s2 x, ForallOrdPairs R (s1++x::s2) -> eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
proof: Proof. intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x H. - reflexivity. - transitivity (f a (f x (fold_right f i (s1++s2)))). + apply Comp; auto. apply IHs1. invlist ForallOrdPairs; auto. + apply TraR. invlist ForallOrdPairs; auto. match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- R a x => rewrite Forall_forall in H0; apply H0 end. apply in_or_app; simpl; auto. Qed.
imports: List Sorted Setoid Basics Morphisms