:: deftheorem defines CPC-Taut INTPRO_1:def 21 :
CPC-Taut = CnCPC ({} MC-wff);