for A being QC-alphabet
for a being Element of free_QC-variables A
for x being Element of bound_QC-variables A holds a <> x