for Al being QC-alphabet
for Al2 being b₁ -expanding QC-alphabet
for f being FinSequence of CQC-WFF Al2
for g being FinSequence of CQC-WFF Al st f = g holds
( Ant f = Ant g & Suc f = Suc g )