obtain ⟨F, hF⟩ := ne
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FrameClass.IsNonempty 𝔽(Ax(L))
h : L ⊢! ⊥
⊢ False
case mk.intro
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
h : L ⊢! ⊥
F : Frame
hF : F ∈ 𝔽(Ax(L))
⊢ False