theorem :: CQC_SIM1:25

for A being QC-alphabet holds SepVar (VERUM A) = VERUM A