For the purposes of giving the procedure for evaluation and explaining the semantics of judgements, we would only need to consider substitution of closed terms for free variables and hence would not need to consider simultaneous substitution or capture. However, for the purpose of specifying inference rules later we shall want to have simultaneous substitution of terms with free variables for free variables. The result of such a substitution is indicated thus:
where 
, 
are variables (not necessarily
distinct) and 
are terms.
It is handy to permit multiple occurrences of the same variable among
the targets for replacements, all but the last of which are ignored.
is the result of replacing
each free occurrence of 
in t by 
for 
,
where 
is 
with j the greatest k such that 
is 
.