Question about substitution notation

[qcfu-bu]

I was trying to follow the examples shown in
https://github.com/andreasabel/strong-normalization/tree/master/coq/well-scoped

When trying to compile the examples, in reduction.v, coq reports that is does not know how to interpret notation (_[_]). From what I understand (_[_]) is the notation used for substitution. When checking its definition in stlc.v, the notation is set to printing only. I was wondering what's the right way to use autosubst's notations?