have claim : ∀ u v, (M,v) ⊨ ρ → relate M β u v → (M,u) ⊨ ρ := by
  intro u v v_rho u_β_v
  have u_ : (M,u) ⊨ (~⌈β⌉~ρ) := by
    simp [modelCanSemImplyForm] at *
    use v
  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
  simp only [modelCanSemImplyForm, Formula.or, evaluatePoint, evaluate] at u_2
  rw [← @or_iff_not_and_not] at u_2
  specialize repl_imp_rho W M u
  aesop
β : 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
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ
β : 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
claim : ∀ (u v : W), (M, v)⊨ρ → relate M β u v → (M, u)⊨ρ
⊢ ∀ (w : W), (∀ φ ∈ [~⌈∗β⌉ψ], evaluate M w φ) → ∀ ψ ∈ [ρ], evaluate M w ψ