proposition: Lemma fold_right_commutes_restr2 : forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) -> eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))).
proof: Proof. intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x i j heqij ?. - apply Comp. + destruct eqA_equiv. apply Equivalence_Reflexive. + eapply fold_right_eqlistA2. * assumption. * reflexivity. - transitivity (f a (f x (fold_right f j (s1++s2)))). + apply Comp; auto. eapply IHs1. * assumption. * invlist ForallOrdPairs; auto. + apply TraR. * invlist ForallOrdPairs; auto. match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- _ => rewrite Forall_forall in H0; apply H0 end. apply in_or_app; simpl; auto. * reflexivity. Qed.
imports: List Sorted Setoid Basics Morphisms