cases φ
σ : Substitution
φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ φ ↔ (subst_in_model σ M, w)⊨φ
case bottom
σ : Substitution
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨subst_in_F σ Formula.bottom ↔ (subst_in_model σ M, w)⊨Formula.bottom

case atom_prop
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝ : ℕ
⊢ (M, w)⊨subst_in_F σ (·a✝) ↔ (subst_in_model σ M, w)⊨·a✝

case neg
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝ : Formula
⊢ (M, w)⊨subst_in_F σ (~a✝) ↔ (subst_in_model σ M, w)⊨(~a✝)

case and
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝¹ a✝ : Formula
⊢ (M, w)⊨subst_in_F σ (a✝¹⋀a✝) ↔ (subst_in_model σ M, w)⊨a✝¹⋀a✝

case box
σ : Substitution
W : Type
M : KripkeModel W
w : W
a✝¹ : Program
a✝ : Formula
⊢ (M, w)⊨subst_in_F σ (⌈a✝¹⌉a✝) ↔ (subst_in_model σ M, w)⊨⌈a✝¹⌉a✝