apply arithmetical_soundness_K4Loeb (T₀ := T₀)
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ ∀ {f : realization L α}, T ⊢! f[β] p
case h
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p