Fix bug introduced by earlier commit on first-order unification of primitive
projections and their expansion, allowing unfolding when it fails.
Cleanup code in reductionops.ml