case star α =>
  have IHα := repl_in_model_rel_iff x ψ α M
  simp_all only [repl_in_P, relate]
  constructor
  all_goals
    apply Relation.ReflTransGen.mono
    intro w v
    rw [IHα w v]
    tauto
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