Now we substitute as far into the term as we can. This is to deal
with terms that contain Coq variables.