simp [consequence_iff, Satisfiable]
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ T ⊨[M] f ↔ ¬Satisfiable M (insert (~f) T)
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) ↔ ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T