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