apply impTaut
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) ψ1
φ : Formula
W : Type
M : KripkeModel W
w : W
ψ1 : Formula
lhs : Evaluate (M, w) φ
impTaut : Evaluate (M, w) φ → Evaluate (M, w) ψ1
⊢ Evaluate (M, w) φ