aesop
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]
no goals