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