simpa [←System.not_consistent_iff_inconsistent] using satisfiable_of_consistent
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
inst✝¹ : ∀ (𝓜 : M), Semantics.Meaningful 𝓜
𝓢 : S
T : Set F
inst✝ : Complete 𝓢 (Semantics.models M T)
⊢ ¬System.Inconsistent 𝓢 → ¬¬Semantics.Satisfiable M T
no goals