rcases Set.not_nonempty_iff_eq_empty.mp A
case mk.intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
f : F
hf : ¬s ⊧ f
A : ¬s.Nonempty
⊢ False
case mk.intro.refl
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
f : F
hf : ¬∅ ⊧ f
A : ¬∅.Nonempty
⊢ False