Takeuchi-Yasugiでは自由変数にtermを代入するという言い方になっている。
Shoenfieldでは代入可能であること(substitutible)の意味を規定して自由変数にtermをreplaceした式
A[a1,...,an]を定義している。
そのあと"substitution"を公理の名前や定理の名前につけている。
字面と内容が一致していると考えているが何か？
http://imgur.com/a/dBTQW