proposition: Lemma fold_right_equivlistA_restr2 : forall s s' i j, NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> equivlistA s s' -> eqB i j -> eqB (fold_right f i s) (fold_right f j s').
proof: Proof. intros s; induction s as [|x l Hrec]. { intros s'; destruct s' as [|a s']; simpl. - intros. assumption. - unfold equivlistA; intros ? ? H H0 H1 H2 **. destruct (H2 a). assert (InA a nil) by auto; inv. } intros s' i j N N' F E eqij; simpl in *. assert (InA x s') as H by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. transitivity (f x (fold_right f j (s1++s2))). - apply Comp; auto. apply Hrec; auto. + inv; auto. + eapply NoDupA_split; eauto. + invlist ForallOrdPairs; auto. + eapply equivlistA_NoDupA_split; eauto. - transitivity (f y (fold_right f i (s1++s2))). + apply Comp; auto. symmetry. apply fold_right_eqlistA2. * assumption. * reflexivity. + symmetry. apply fold_right_commutes_restr2. * symmetry. assumption. * apply ForallOrdPairs_inclA with (x::l); auto. red; intros; rewrite E; auto. Qed.
imports: List Sorted Setoid Basics Morphisms