for A being QC-alphabet
for t being QC-symbol of A
for p being Element of CQC-WFF A st x. t in still_not-bound_in p holds
t < index p