make ARM+ARM_HYP proofs work for smaller irq_len

[lsf37]

• Remove remaining use of direct numeral related to irq_len. The lemma happened to work for irq_len >= 8, but not for smaller irq_len.

• Improve sys-init example: the example assumes an irq type of at least 8 bits. Some AArch32 boards only use 7 bit. Use smaller numbers in the example so that the example happens to work on those boards as well.