cases α
x : ℕ
ψ : Formula
α : Program
W : Type
M : KripkeModel W
w v : W
⊢ relate M (repl_in_P x ψ α) w v ↔ relate (repl_in_model x ψ M) α w v
case atom_prog
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝ : ℕ
⊢ relate M (repl_in_P x ψ (·a✝)) w v ↔ relate (repl_in_model x ψ M) (·a✝) w v

case sequence
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝¹ a✝ : Program
⊢ relate M (repl_in_P x ψ (a✝¹;'a✝)) w v ↔ relate (repl_in_model x ψ M) (a✝¹;'a✝) w v

case union
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝¹ a✝ : Program
⊢ relate M (repl_in_P x ψ (a✝¹⋓a✝)) w v ↔ relate (repl_in_model x ψ M) (a✝¹⋓a✝) w v

case star
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝ : Program
⊢ relate M (repl_in_P x ψ (∗a✝)) w v ↔ relate (repl_in_model x ψ M) (∗a✝) w v

case test
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w v : W
a✝ : Formula
⊢ relate M (repl_in_P x ψ (?'a✝)) w v ↔ relate (repl_in_model x ψ M) (?'a✝) w v