case sequence α β =>
  have IHα := repl_in_model_rel_iff x ψ α M
  have IHβ := repl_in_model_rel_iff x ψ β M
  simp_all only [repl_in_P, relate]
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
α β : Program
⊢ relate M (repl_in_P x ψ (α;'β)) w v ↔ relate (repl_in_model x ψ M) (α;'β) w v
no goals