new theorem about exprD' and equal (but different) variable
environments.