simp only [satisfiable, not_exists, not_forall, exists_prop, setCanSemImplySet, semImpliesSets, forall_eq]
case mp
X : List Formula
φ : Formula
⊢ ¬satisfiable (X ∪ [~φ]) → X⊨[φ]
case mp
X : List Formula
φ : Formula
⊢ (∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x), ∃ x_3 ∈ X ∪ [~φ], ¬evaluate x_1 x_2 x_3) → semImpliesLists X [φ]