for Al being QC-alphabet
for k being Nat
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds CQC_Subst (ll,Sub) is CQC-variable_list of k,Al