:: deftheorem defines IPC-Taut INTPRO_1:def 16 :
IPC-Taut = CnIPC ({} MC-wff);