tauto
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : evaluate M w (subst_in_F σ φ) ↔ evaluate (subst_in_model σ M) w φ
⊢ ¬evaluate M w (subst_in_F σ φ) ↔ ¬evaluate (subst_in_model σ M) w φ
no goals