simpa using hu
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ T
hu : ¬Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ¬Semantics.Satisfiable M ↑(insert (~f) u)
no goals