We show how a well-known superposition-based inference system for
first-order equational logic can be used almost directly as a
decision procedure for various theories including lists, arrays,
extensional arrays and combinations of them. We also give a
superposition-based decision procedure for homomorphism.
