theorem :: CQC_THE1:22

Proof_Step_Kinds is finite