Generalized substitution lemma stated, with some sanity checks.