$\begin{array} & \mbox{For all } M, x \mbox{ and } y \notin FV(xM), \mbox{there exists } M^\prime \mbox{ such that } \\ y \mbox{ is neither free nor bound in } M^\prime \mbox{ and } x \mbox{ is not bound in } M^\prime \mbox{, and } \\ M \rhd_{\alpha0} M^\prime, \qquad [y/x]M \rhd_{\alpha0} [y/x]M^\prime \end{array}$

$\begin{array} & M ≡ x \mbox{ の時 } M^\prime ≡ x \\ \mbox{ここで } [y/x]M ≡ y \mbox{, } [y/x]M^\prime ≡ y \mbox{ なので } [y/x]M ≡ [y/x]M^\prime \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$\begin{array} & M ≡ y \mbox{ の時 } M^\prime ≡ y \\ \mbox{ここで } [y/x]M ≡ y \mbox{, } [y/x]M^\prime ≡ y \mbox{ なので } [y/x]M ≡ [y/x]M^\prime \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$\begin{array} & M ≡ a \mbox{ の時 } M^\prime ≡ a \\ \mbox{ここで } [y/x]M ≡ a \mbox{, } [y/x]M^\prime ≡ a \mbox{ なので } [y/x]M ≡ [y/x]M^\prime \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$\begin{array} & M^\prime ≡ λa.[a/x]L \mbox{ ;; } a \notin FV(L) \\ [y/x]M ≡ [y/x]λx.L ≡ λx.L ~ \cdots (A)\\ [y/x]M^\prime ≡ [y/x]λa.[a/x]L ≡ λa.[y/x][a/x]L \\ \mbox{;; Lemma1.16(e) より } \\ ≡ λa.[([y/x]a)/x]L ≡ λa.[a/x]L ~ \cdots (B) \\ \mbox{帰納法により } L^\prime \rhd_{\alpha0} [a^\prime/x^\prime]L^\prime \\ \mbox{が正しいと仮定して以下を導きます} \\ \mbox{(A), (B) は定義から } λx.L \rhd_{\alpha0} λa.[a/x]L \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$\begin{array} & M^\prime ≡ λa.[a/y]L, ~ a \notin FV(L) \\ [y/x]M ≡ [y/x]λy.L ≡ λz.[y/x][z/y]L \\ \mbox{;; Lemma1.16(c) より } \\ \mbox{;; } [P/x][Q/y]M ≡ [([P/x]Q)/y][P/x]M, ~ y \notin FV(P) \\ ≡ λz.[([y/x]z)/y][y/x]L ≡ λz.[z/y][y/x]L \\ \mbox{;; Lemma1.16(a) より } \\ \mbox{;; } [P/v][v/x]M ≡ [P/x]M, ~ v \notin FV(M) \\ \mbox{;; 条件 } y \notin FV(xM) \mbox{ より} \\ ≡ λz.[z/x]L ~ \cdots (A) \\ [y/x]M^\prime ≡ [y/x]λa.[a/y]L ≡ λa.[y/x][a/y]L \\ \mbox{;; 同様に Lemma1.16(c) より} \\ ≡ λa.[([y/x]a)/y][y/x]L ≡ λa.[a/y][y/x]L \\ \mbox{;; 同様に Lemma1.16(a) より } \\ ≡ λa.[a/x]L ~ \cdots (B) \\ \mbox{帰納法により } [z^\prime/x^\prime]L^\prime \rhd_{\alpha0} [a^\prime/x^\prime]L^\prime \\ \mbox{が正しいと仮定して以下を導きます} \\ \mbox{(A),(B) より } λz.[z/x]L \rhd_{\alpha0} λa.[a/x]L \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$\begin{array} & M^\prime ≡ λb.[b/a]L \mbox{ ;; } b \notin FV(L) \\ [y/x]M ≡ [y/x]λa.L ≡ λa.[y/x]L ~ \cdots (A) \\ \mbox{(条件より} y \notin FV(L) \mbox{ なので 1.12(g) はおこらない)} \\ [y/x]M^\prime ≡ [y/x]λb.[b/a]L ≡ λb.[y/x][b/a]L \\ \mbox{;; Lemma1.16(d) } [P/x][Q/y]M ≡ [Q/y][P/x]M ~ y \notin FV(P), ~ x \notin FV(Q) \mbox{ より} \\ \mbox{;; } a \notin FV(y), ~ x \notin FV(b) \mbox{ なので}\\ ≡ λb.[b/a][y/x]L ~ \cdots (B) \\ \mbox{(条件より} y \notin FV(L) \mbox{ なので 1.12(g) はおこらない)} \\ \mbox{帰納法により } [y^\prime/x^\prime]L^\prime \rhd_{\alpha0} [b^\prime/a^\prime][y^\prime/x^\prime]L^\prime \\ \mbox{が正しいと仮定して以下を導きます} \\ \mbox{(A), (B) は定義から } λa.[y/x]L \rhd_{\alpha0} λb.[b/a][y/x]L \\ \therefore [y/x]M \rhd_{\alpha0} [y/x]M^\prime \\ \end{array}$

$\begin{array} & M^\prime ≡ (RS) \mbox{ とする} \\ [y/x]M ≡ [y/x](PQ) ≡ ([y/x]P [y/x]Q) \\ [y/x]M^\prime ≡ [y/x](RS) ≡ ([y/x]R [y/x]S) \\ \mbox{帰納法により } \\ [y^\prime/x^\prime]P^\prime \rhd_{\alpha0} [y^\prime/x^\prime]R^\prime, ~ [y^\prime/x^\prime]Q^\prime \rhd_{\alpha0} [y^\prime/x^\prime]S^\prime \mbox{ が正しいと仮定して以下を導きます} \\ (PQ) \rhd_{\alpha0} (RS) \end{array}$

$\mbox{(1)〜(7) より 条件の時、} M \rhd_{\alpha0} M^\prime, ~ [y/x]M \rhd_{\alpha0} [y/x]M^\prime.$