Proof_Step_Kinds is finite