:: deftheorem defines QScope SUBSTUT2:def 3 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for Sub being CQC_Substitution of Al holds QScope (p,x,Sub) = [[p,((CFQ Al) . [(All (x,p)),Sub])],x];