So substitution has to be defined inductively, but we have to give up something.
