proposition: Lemma fold_right_equivlistA2 : forall s s' i j, NoDupA s -> NoDupA s' -> eqB i j -> equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s').
proof: Proof. red in Tra. intros; apply (fold_right_equivlistA_restr2 (R:=fun _ _ => True)); repeat red; auto. apply ForallPairs_ForallOrdPairs; try red; auto. Qed.
imports: List Sorted Setoid Basics Morphisms