tauto
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
φ : Formula
IH : evaluate M w (repl_in_F x ψ φ) ↔ evaluate (repl_in_model x ψ M) w φ
⊢ ¬evaluate M w (repl_in_F x ψ φ) ↔ ¬evaluate (repl_in_model x ψ M) w φ
no goals