theorem :: CQC_SIM1:36

for A being QC-alphabet holds SepQuadruples (VERUM A) = {[(VERUM A),(0 A),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}