proposition: Lemma fold_right_equivlistA_restr : forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
proof: Proof. intros s; induction s as [|x l Hrec]. - intros s'; destruct s' as [|a s']; simpl. + intros; reflexivity. + unfold equivlistA; intros H H0 H1 H2. destruct (H2 a). assert (InA a nil) by auto; inv. - intros s' N N' F E; 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 i (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. reflexivity. * symmetry; apply fold_right_commutes_restr. apply ForallOrdPairs_inclA with (x::l); auto. red; intros; rewrite E; auto. Qed.
imports: List Sorted Setoid Basics Morphisms