have IH2 := repl_in_model_sat_iff x ψ φ2 M w
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ1 φ2 : Formula
IH1 : (M, w)⊨repl_in_F x ψ φ1 ↔ (repl_in_model x ψ M, w)⊨φ1
IH2 : (M, w)⊨repl_in_F x ψ φ2 ↔ (repl_in_model x ψ M, w)⊨φ2
⊢ (M, w)⊨repl_in_F x ψ (φ1⋀φ2) ↔ (repl_in_model x ψ M, w)⊨φ1⋀φ2