Demand: Document why we need three additional equations of multSubDmd

Just a few comments and a few changes to .gitignore to ignore build directories leading with _.

Originally part of !7599 (merged), then of !7609 (closed), then of !7633 (closed). But since we probably won't merge !7633 (closed) and these two commits are uncontroversial, I'll just put them up separately.