Substitution by structural recursion
A more tutorial-paced presentation of the same/related material is available in:
Roy L. Crole: Basic Category Theory for Models of Syntax. Generic Programming 2003: 133-177. This should help.