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
⊢ relate M (repl_in_P x ψ (∗α)) w v ↔ relate (repl_in_model x ψ M) (∗α) w v
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
⊢ Relation.ReflTransGen (relate M (repl_in_P x ψ α)) w v ↔ Relation.ReflTransGen (relate (repl_in_model x ψ M) α) w v