:: deftheorem defines S4-Taut INTPRO_1:def 24 :
S4-Taut = CnS4 ({} MC-wff);