simp [Kripke.ValidOnFrameClass, Kripke.ValidOnFrame]
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
⊢ 𝔽(Ax(L)) ⊧ p → L ⊢! p
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
p : Formula α
inst✝¹ : Consistent L
inst✝ : Canonical L
⊢ (∀ F ∈ 𝔽(Ax(L)), ∀ (V : Valuation F.World α), Kripke.ValidOnModel { Frame := F, Valuation := V } p) → L ⊢! p