for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds still_not-bound_in (rng f) = still_not-bound_in f