for A being QC-alphabet
for x being bound_QC-variable of A ex t being QC-symbol of A st x. t = x