proposition: Lemma fold_right_eqlistA : forall s s', eqlistA s s' -> eqB (fold_right f i s) (fold_right f i s').
proof: Proof. induction 1; simpl; auto with relations. apply Comp; auto. Qed.
imports: List Sorted Setoid Basics Morphisms