tauto
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
no goals