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