:: deftheorem defines @ SUBSTUT1:def 4 :
for A being QC-alphabet
for l being FinSequence of bound_QC-variables A holds @ l = l;