exact IHφ
σ : 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