simp [modelCanSemImplyForm, evaluatePoint, formCanSemImplyForm, semImpliesLists] at *
β : 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)⊨(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
⊢ (M, u)⊨ρ⋀repl_in_F x ρ σ0⋁repl_in_F x ρ σ1
β : Program
σ0 σ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (~⌈β⌉~·x)≡(~(~(·x)⋀σ0)⋀(~σ1))
W : Type
M : KripkeModel W
u v : W
v_rho : evaluate M v ρ
u_β_v : relate M β u v
repl_equiv : (~⌈β⌉~ρ)≡(~(~ρ⋀repl_in_F x ρ σ0)⋀(~repl_in_F x ρ σ1))
nox : repl_in_P x ρ β = β
repl_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w (repl_in_F x ρ σ1) → evaluate M w ρ
notPsi_imp_rho : ∀ (W : Type) (M : KripkeModel W) (w : W), ¬evaluate M w ψ → evaluate M w ρ
u_ : (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)
⊢ (evaluate M u ρ → ¬evaluate M u (repl_in_F x ρ σ0)) → evaluate M u (repl_in_F x ρ σ1)