theorem :: HENMODEL:8

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al st X \/ {p} |- q holds
ex g being FinSequence of CQC-WFF Al st
( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )