intro W M w lhs ψ psi_in_psi
φ ψ : Formula
impTaut : φ⊨ψ
⊢ [φ]⊨[ψ]
φ ψ✝ : Formula
impTaut : φ⊨ψ✝
W : Type
M : KripkeModel W
w : W
lhs : ∀ φ_1 ∈ [φ], evaluate M w φ_1
ψ : Formula
psi_in_psi : ψ ∈ [ψ✝]
⊢ evaluate M w ψ