Ban axioms in non-axiom Hermes annotations

Ban Lean `axiom`s or other Lean constructs which amount to axiomatic statements. Hermes annotations marked as `unsafe(axiom)` are allowed to use `axiom`s.