:: deftheorem defines -Cast QC_TRANS:def 4 :
for Al being QC-alphabet
for Al2 being b₁ -expanding QC-alphabet
for x being bound_QC-variable of Al holds Al2 -Cast x = x;