for k being Nat
for A being QC-alphabet
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds still_not-bound_in (P ! l) = still_not-bound_in l