for Al being QC-alphabet
for k being Nat
for P, P9 being QC-pred_symbol of k,Al
for ll, ll9 being CQC-variable_list of k,Al
for Sub, Sub9 being CQC_Substitution of Al st Sub_the_arguments_of (Sub_P (P,ll,Sub)) = Sub_the_arguments_of (Sub_P (P9,ll9,Sub9)) holds
ll = ll9