intro F hF V w
case hMdp
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ : Formula α
hpq✝ : L ⊢ p✝ ⟶ q✝
hp✝ : L ⊢ p✝
ihpq : 𝔽(Ax(L)) ⊧ p✝ ⟶ q✝
ihp : 𝔽(Ax(L)) ⊧ p✝
⊢ 𝔽(Ax(L)) ⊧ q✝
case hMdp
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
p p✝ q✝ : Formula α
hpq✝ : L ⊢ p✝ ⟶ q✝
hp✝ : L ⊢ p✝
ihpq : 𝔽(Ax(L)) ⊧ p✝ ⟶ q✝
ihp : 𝔽(Ax(L)) ⊧ p✝
F : Frame' α
hF : F ∈ 𝔽(Ax(L))
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ w ⊧ q✝