:: deftheorem defines Proof_Step_Kinds_IPC INTPRO_2:def 2 :
Proof_Step_Kinds_IPC = { k where k is Nat : k <= 10 } ;