for A being QC-alphabet
for p being QC-formula of A st p is universal holds
still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)}