intro F hF V w w' _
case hNec
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
hp✝ : L ⊢ p✝
ih : 𝔽(Ax(L)) ⊧ p✝
⊢ 𝔽(Ax(L)) ⊧ □p✝
case hNec
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ : Formula α
hp✝ : L ⊢ p✝
ih : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
w' : { Frame := F, Valuation := V }.Frame.World
a✝ : w ≺ w'
⊢ Satisfies { Frame := F, Valuation := V } w' p✝