CLTT読書会 - yoshitake-hのブログ

3.2 節．Lemma 3.2.4 の downwards の証明で紛糾．
$L=L',\, x=y\,\vdash\, L[x/y]=L'[x/y]$
が得られればよいところまではわかったが，これの導き方がわからなかった．
これは Lemma 3.2.3 の証明中の後半（とばした部分）にある議論を用いて得られる．すなわち，replacement より
$L=L',\, x=y\,\vdash\, L[z/y][x/z]=L[z/y][y/z]\quad \equiv (L[x/y]=L)$
$L=L',\, x=y\,\vdash\, L'[x/y]=L'$
が得られるので，これらと symmetry, transitivity から．