$\begin{array} & N' ≡ [M/x]N \\ [M/x][N/y]X ≡ [N'/y][M/x]X \end{array}$

$\begin{array} & X ≡ λx.fxy \\ M ≡ a \mbox{ ;; a variable not otherwise used), } \\ N ≡ x. \\ \\ \begin{array}{ll} N' &≡ [M/x]N \\ &≡ [a/x]x \\ &≡ a \\ X\ast &≡ [M/x][N/y]X \\ &≡ [a/x][x/y]λx.fxy \\ &≡ [a/x]λz.fzx \\ &≡ λz.fza \\ X\# &≡ [N'/y][M/x]X \\ &≡ [N'/y][a/x]λx.fxy \\ &≡ [N'/y]λx.fxy \\ &≡ [a/y]λx.fxy \\ &≡ λx.fxa \\ \end{array} \\ \end{array}$