simp only [satisfiable, setCanSemImplySet, semImpliesSets] at hyp
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : satisfiable (X ∪ [~φ])
⊢ False
case mpr
X : List Formula
φ : Formula
X_φ : X⊨[φ]
hyp : ∃ W M w, ∀ φ_1 ∈ X ∪ [~φ], evaluate M w φ_1
⊢ False