Implement `NumberSentences` as a Pyk pass

[Baltoli]

@PetarMax requests that we implement the generation of unique IDs for rules in Pyk, so that generated rules can get IDs compatible with those generated by the existing frontend. I've done some digging into this, and I think what we need to do is:

• Implement alpha-renaming of variables over KInner (https://github.com/runtimeverification/k/blob/master/kernel/src/main/java/org/kframework/compile/NormalizeVariables.java) in a way that's compatible with the frontend. Should be easy to generate unit tests from the existing Java code's behaviour.
• Ensure that printing of rules in Pyk is compatible, such that hashing a printed rule with the same hash function as the Java frontend does with produce the same result.
• Filter rule attributes in the same way as the frontend.
• Combine these implementations into a compatible implementation of number_sentences; also unit-testable from the frontend I think.

[Baltoli]

@tothtamas28 suggests just reusing rule labels as a way of getting unique identifiers for claims.

@dwightguth: there are a couple of different types of uniqueness here that need to be considered; uniqueness of axioms and uniqueness of rules. These are not 1:1 with each other; clarify exactly what is required here.