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