theorem Th37: :: CALCUL_1:37

for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al st 1 < len f & 1 < len g & Ant (Ant f) = Ant (Ant g) & 'not' (Suc (Ant f)) = Suc (Ant g) & Suc f = Suc g & |- f & |- g holds
|- (Ant (Ant f)) ^ <*(Suc f)*>