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