have u_ : (M,u) ⊨ (~⌈β⌉~ρ) := by
  simp [modelCanSemImplyForm] at *
  use v
β : 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
⊢ (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)⊨(~⌈β⌉~ρ)
⊢ (M, u)⊨ρ