theorem LO.ProvabilityLogic.N.arithmetical_soundness {L : FirstOrder.Language} [L.ReferenceableBy L] [L.DecidableEq] {T U : FirstOrder.Theory L} [T ⪯ U] {𝔅 : FirstOrder.ProvabilityAbstraction.Provability T U} [𝔅.HBL1] {A : Modal.Formula ℕ} (h : Modal.N ⊢ A) {f : Realization 𝔅} : U ⊢ ↑f A