D5: conditional subtraction on the declared free domain

The domain condition in part (a) is substantive: if a desired pair or reversed free product lies outside $D_{\mathrm{decl}}$, a free enlargement must be proved before these formulas can be applied to it.