have u_2 : (M, u) ⊨ (ρ ⋀ repl_in_F x ρ σ0) ⋁ (repl_in_F x ρ σ1) := by
  have repl_equiv := repl_in_F_equiv x ρ beta_equiv
  simp only [repl_in_F, beq_self_eq_true, reduceIte, Formula.or] at repl_equiv
  have nox : repl_in_P x ρ β = β := repl_in_P_non_occ_eq x_notin_beta
  rw [nox] at repl_equiv
  rw [equiv_iff _ _ repl_equiv] at u_
  simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
  tauto
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
⊢ (M, u)⊨ρ
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(·x)⋀σ0⋁σ1
repl_imp_rho : repl_in_F x ρ σ1⊨ρ
notPsi_imp_rho : (~ψ)⊨ρ
W : Type
M : KripkeModel W
u v : W
v_rho : (M, v)⊨ρ
u_β_v : relate M β u v
u_ : (M, u)⊨(~⌈β⌉~ρ)
u_2 : (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
⊢ (M, u)⊨ρ