for A being QC-alphabet
for H being Element of QC-WFF A
for k being Nat
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V