induction w_bS_v using Relation.ReflTransGen.head_induction_on
case intro.intro
β : 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 v : W
w_bS_v : Relation.ReflTransGen (relate M β) w v
v_Psi : ¬evaluate M v ψ
⊢ evaluate M w ρ
case intro.intro.refl
β : 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 v : W
v_Psi : ¬evaluate M v ψ
⊢ evaluate M v ρ

case intro.intro.head
β : 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 v : W
v_Psi : ¬evaluate M v ψ
a✝¹ c✝ : W
h'✝ : relate M β a✝¹ c✝
h✝ : Relation.ReflTransGen (relate M β) c✝ v
a✝ : evaluate M c✝ ρ
⊢ evaluate M a✝¹ ρ