intro W M w v
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
⊢ repl_in_P x ψ α1≡ᵣrepl_in_P x ψ α2
α1 α2 : Program
x : ℕ
ψ : Formula
hyp : α1≡ᵣα2
W : Type
M : KripkeModel W
w v : W
⊢ relate M (repl_in_P x ψ α1) w v ↔ relate M (repl_in_P x ψ α2) w v