simp [set_meaningful_iff_nonempty, satisfiableSet_iff_models_nonempty]
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
⊢ Satisfiable M T ↔ Meaningful (models M T)
no goals