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