intro hyp
X : Finset Formula
l : List Formula
⊢ Satisfiable (X ∪ {bigCon (List.map (fun x => ~x) l)}) → ∀ φ ∈ l, Satisfiable (X ∪ {~φ})
X : Finset Formula
l : List Formula
hyp : Satisfiable (X ∪ {bigCon (List.map (fun x => ~x) l)})
⊢ ∀ φ ∈ l, Satisfiable (X ∪ {~φ})