theorem :: CQC_SIM1:37

for A being QC-alphabet
for k being Nat
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}