:: deftheorem defines SepVar CQC_SIM1:def 11 :
for A being QC-alphabet
for p being Element of CQC-WFF A holds SepVar p = SepFunc (p,(index p),(id (bound_QC-variables A)));