$\mbox{ (c) If no variables which occur free in M or N are bound in X }$

$\begin{array} & X ≡ λz.Y \mbox{ と置く} \end{array}$

$\begin{array} & \mbox{ z ≡ y の時} & & \\ \begin{array}{lll} X\ast &≡ [M/x][N/y]λz.Y & \mbox{ ;; ここで } z ≡ y \mbox{ なので} \\ &≡ [M/x][N/y]λy.Y & \mbox{ ;; Case 3 (a) より} \\ &≡ [M/x]λy.Y & \mbox{ ;; ここでもともとの前提 (c) から} \\ && \mbox{ ;; y is not free in M なので Case 3 (b) (i) より} \\ &≡ λy.[M/x]Y \\ X\# &≡ [N'/y][M/x]λz.Y & \mbox{ ;; ここで } z ≡ y \mbox{ なので} \\ &≡ [N'/y][M/x]λy.Y & \mbox{ ;; ここで同様にもともとの前提 (c) から} \\ && \mbox{ ;; y is not free in M なので Case 3 (b) (i) より} \\ &≡ [N'/y]λy.[M/x]Y & \mbox{ ;; Case 3 (a) より} \\ &≡ λy.[M/x]Y \\ \end{array} \\ \therefore X\ast ≡ X\#. \end{array}$

$\begin{array} & \mbox{ z ≡ x の時} \\ \begin{array}{lll} X\ast &≡ [M/x][N/y]λz.Y & \mbox{ ;; ここで } z ≡ x \mbox{ なので} \\ &≡ [M/x][N/y]λx.Y & \mbox{ ;; ここでもともとの前提 (c) から} \\ && \mbox{ x is not free in N なので Case 3 (b) (i) より} \\ &≡ [M/x]λx.[N/y]Y & \mbox{ ;; Case 3 (a) より} \\ &≡ λx.[N/y]Y \\ X\# &≡ [N'/y][M/x]λz.Y & \mbox{ ;; ここで } z ≡ x \mbox{ なので} \\ &≡ [N'/y][M/x]λx.Y & \mbox{ ;; Case 3 (a) より} \\ &≡ [N'/y]λx.Y & \mbox{ ;; N' について N であらわすと} \\ &≡ [([M/x]N)/y]λx.Y & \mbox{ ;; ここでもともとの前提 (c) から}\\ && \mbox{ x is not free in N なので [M/x]N ≡ N より} \\ &≡ [N/y]λx.Y & \mbox{ ;; ここで同様にもともとの前提 (c) から} \\ && \mbox{ x is not free in N なので Case 3 (b) (i) より} \\ &≡ λx.[N/y]Y \\ \end{array} \\ \therefore X\ast ≡ X\#. \end{array}$