Tidy up substitutions

The new simplifer stuff exposed the fact that the invariants on the
TvSubstEnv and IdSubstEnv were insufficiently explicit.  (Resulted in
a bug found by Sam Brosnon.)

This patch fixes the bug, and tries to document the invariants pretty
thoroughly. See
	Note [Extending the TvSubst] in Type
	Note [Extenting the Subst]   in CoreSubst

(Most of the new lines are comments.)