intro W M w
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
⊢ repl_in_F x ψ φ1≡repl_in_F x ψ φ2
φ1 φ2 : Formula
x : ℕ
ψ : Formula
hyp : φ1≡φ2
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (repl_in_F x ψ φ1) ↔ evaluate M w (repl_in_F x ψ φ2)