:: deftheorem defines -Cast QC_TRANS:def 6 :
for Al being QC-alphabet
for Al2 being b₁ -expanding QC-alphabet
for k being Nat
for l being CQC-variable_list of k,Al holds Al2 -Cast l = l;