exact fortysix W M u1 u2 w_rho u1_b_u2
β : 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 : ρ⊨ψ
fortysix : ∀ (W : Type) (M : KripkeModel W) (w v : W), (M, w)⊨ρ → relate M β w v → (M, v)⊨ρ
W : Type
M : KripkeModel W
w v u1 u2 : W
u1_b_u2 : relate M β u1 u2
h✝ : Relation.ReflTransGen (relate M β) u2 v
IH : evaluate M u2 ρ → evaluate M v ψ
w_rho : evaluate M u1 ρ
⊢ evaluate M u2 ρ
no goals