cases α
σ : Substitution
α : Program
W : Type
M : KripkeModel W
w v : W
⊢ relate M (subst_in_P σ α) w v ↔ relate (subst_in_model σ M) α w v
case atom_prog
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝ : ℕ
⊢ relate M (subst_in_P σ (·a✝)) w v ↔ relate (subst_in_model σ M) (·a✝) w v

case sequence
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝¹ a✝ : Program
⊢ relate M (subst_in_P σ (a✝¹;'a✝)) w v ↔ relate (subst_in_model σ M) (a✝¹;'a✝) w v

case union
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝¹ a✝ : Program
⊢ relate M (subst_in_P σ (a✝¹⋓a✝)) w v ↔ relate (subst_in_model σ M) (a✝¹⋓a✝) w v

case star
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝ : Program
⊢ relate M (subst_in_P σ (∗a✝)) w v ↔ relate (subst_in_model σ M) (∗a✝) w v

case test
σ : Substitution
W : Type
M : KripkeModel W
w v : W
a✝ : Formula
⊢ relate M (subst_in_P σ (?'a✝)) w v ↔ relate (subst_in_model σ M) (?'a✝) w v