Substitution

Substitution is a special kind of replacement: $M\{x\mapsto N\}$ means replace all free occurrences of $x$ in $M$ by the term $N$.

A very useful property of substitution is the Substitution Lemma:

If $x\notin FV(P)$:

$$(M\{x\mapsto N\})\{y\mapsto P\} = (M\{y\mapsto P\})\{x\mapsto N\{y\mapsto P\}\}$$ (14)