rintro ⟨f, hf⟩
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
⊢ Meaningful s → s.Nonempty
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
⊢ s.Nonempty