for Al being QC-alphabet
for l1 being FinSequence of QC-variables Al st rng l1 c= bound_QC-variables Al holds
still_not-bound_in l1 = rng l1