tauto
β : Program
χ0 χ1 ρ ψ : Formula
x : ℕ
x_notin_beta : x ∉ voc β
beta_equiv : (⌈β⌉·x)≡(~(~(·x)⋀χ0)⋀(~χ1))
rho_imp_psi : ρ⊨ψ
W : Type
M : KripkeModel W
w v : W
w_rho : evaluate M w ρ
w_β_v : relate M β w v
rho_imp_repl : ρ⊨(~(~repl_in_F x ρ χ0)⋀(~repl_in_F x ρ χ1))
by_ass : ¬evaluate M w (repl_in_F x ρ χ0) → evaluate M w (repl_in_F x ρ χ1)
obvious : evaluate M w ρ
⊢ (evaluate M w ρ → ¬evaluate M w (repl_in_F x ρ χ0)) → evaluate M w (repl_in_F x ρ χ1)
no goals