Can someone explain how ,Coq development does not treat terms modulo α-conversion, therefore the ,substitution a[x ← b] can capture variables. However, it is capture-avoiding if b is
closed, and this suffices to define evaluation and reduction of closed source terms.
From
First, if b is closed, then by definition it has no free variables, so a cannot capture any of them.
Second, notice that, during an evaluation, all the substituted terms are closed. Consider a reduction step T -> T'. You can prove by induction over its derivation the following property: “if T is a closed term, then T' is closed and no variables were captured”. Indeed, suppose that T is closed and is an application A B. There are two cases. If T is a redex (i.e., A = \x.a), then T' = a[x <- B] which satisfies the property. Otherwise, either A or B gets reduced (e.g., A -> A'), so T' = A' B' which satisfies the property by induction.
The important point is that the above reasoning only works because we are talking about evaluation and not strong normalization. In the latter case, you would have to consider a third case in the derivation: T is an abstraction \x.t where t is an open term, which breaks the induction.