have IH2 := substitutionLemma σ φ2 M w
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2
σ : Substitution
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨subst_in_F σ φ1 ↔ (subst_in_model σ M, w)⊨φ1
IH2 : (M, w)⊨subst_in_F σ φ2 ↔ (subst_in_model σ M, w)⊨φ2
⊢ (M, w)⊨subst_in_F σ (φ1⋀φ2) ↔ (subst_in_model σ M, w)⊨φ1⋀φ2