:: deftheorem defines are_similar CQC_SIM1:def 14 :
for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( p,q are_similar iff SepVar p = SepVar q );