:: deftheorem defines MP-variables MODAL_1:def 3 :
MP-variables = [:{3},NAT:];