:: deftheorem defines Proof_Step_Kinds CQC_THE1:def 3 :
Proof_Step_Kinds = { k where k is Nat : k <= 9 } ;