  When building a cylindrical algebraic decomposition (CAD) savings can be made
in the presence of an equational constraint (EC): an equation logically implied
by a formula.
  The present paper is concerned with how to use multiple ECs, propagating
those in the input throughout the projection set. We improve on the approach of
McCallum in ISSAC 2001 by using the reduced projection theory to make savings
in the lifting phase (both to the polynomials we lift with and the cells lifted
over). We demonstrate the benefits with worked examples and a complexity
analysis.
