simp [Satisfiable, realizeSet_iff, Valid, Finset.map_disj]
M : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
𝓢 : Semantics F M
inst✝¹ : Tarski M
inst✝ : DecidableEq F
t : Finset F
⊢ ¬Satisfiable M ↑t ↔ Valid M (⋁Finset.image (fun x => ~x) t)
no goals