simp at *
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1
ψ1 : Formula
psi1_in_setpsi : ψ1 ∈ {ψ}
impTaut : (∀ φ_1 ∈ {φ}, Evaluate (M, w) φ_1) → ∀ ψ_1 ∈ {ψ}, Evaluate (M, w) ψ_1
⊢ Evaluate (M, w) ψ1
φ ψ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
psi1_in_setpsi : ψ1 = ψ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ
⊢ Evaluate (M, w) ψ1