Theorem: bigCon_union_sat_down (Bml/bigConDis.lean)

State before:
X : Finset Formula
l : List Formula
⊢ Satisfiable (X ∪ {bigCon l}) → ∀ φ ∈ l, Satisfiable (X ∪ {φ})
Tactic:
simp at *
State after:
X : Finset Formula
l : List Formula
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x),
    (∀ φ ∈ l, Evaluate (x_1, x_2) φ) →
      (∀ a ∈ X, Evaluate (x_1, x_2) a) → ∀ φ ∈ l, ∃ W M w, Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a

State before:
X : Finset Formula
l : List Formula
⊢ ∀ (x : Type) (x_1 : KripkeModel x) (x_2 : x),
    (∀ φ ∈ l, Evaluate (x_1, x_2) φ) →
      (∀ a ∈ X, Evaluate (x_1, x_2) a) → ∀ φ ∈ l, ∃ W M w, Evaluate (M, w) φ ∧ ∀ a ∈ X, Evaluate (M, w) a
Tactic:
tauto
State after:
no goals