have by_ass : (M,w) ⊨ (repl_in_F x ρ) (χ0 ⋁ χ1) := by apply rho_imp_repl; simp; exact w_rho; simp
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
⊢ (M, w)⊨⌈β⌉ρ
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(·x)⋀χ0⋁χ1
rho_imp_repl : ρ⊨repl_in_F x ρ (χ0⋁χ1)
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : (M, w)⊨ρ
w_β_v : relate M β w v
by_ass : (M, w)⊨repl_in_F x ρ (χ0⋁χ1)
⊢ (M, w)⊨⌈β⌉ρ