rcases hyp with ⟨W, M, w, sat⟩
X : Finset Formula
l : List Formula
hyp : Satisfiable (X ∪ {bigCon (List.map (fun x => ~x) l)})
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
case intro.intro.intro
X : Finset Formula
l : List Formula
W : Type
M : KripkeModel W
w : W
sat : ∀ φ ∈ X ∪ {bigCon (List.map (fun x => ~x) l)}, Evaluate (M, w) φ
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})