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