have IHα := substitutionLemmaRel σ α M w
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ
σ : Substitution
W : Type
M : KripkeModel W
w : W
α : Program
φ : Formula
IHα : ∀ (v : W), relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
⊢ (M, w)⊨subst_in_F σ (⌈α⌉φ) ↔ (subst_in_model σ M, w)⊨⌈α⌉φ