cases φ
x : ℕ
ψ φ : Formula
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨repl_in_F x ψ φ ↔ (repl_in_model x ψ M, w)⊨φ
case bottom
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
⊢ (M, w)⊨repl_in_F x ψ Formula.bottom ↔ (repl_in_model x ψ M, w)⊨Formula.bottom

case atom_prop
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝ : ℕ
⊢ (M, w)⊨repl_in_F x ψ (·a✝) ↔ (repl_in_model x ψ M, w)⊨·a✝

case neg
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝ : Formula
⊢ (M, w)⊨repl_in_F x ψ (~a✝) ↔ (repl_in_model x ψ M, w)⊨(~a✝)

case and
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝¹ a✝ : Formula
⊢ (M, w)⊨repl_in_F x ψ (a✝¹⋀a✝) ↔ (repl_in_model x ψ M, w)⊨a✝¹⋀a✝

case box
x : ℕ
ψ : Formula
W : Type
M : KripkeModel W
w : W
a✝¹ : Program
a✝ : Formula
⊢ (M, w)⊨repl_in_F x ψ (⌈a✝¹⌉a✝) ↔ (repl_in_model x ψ M, w)⊨⌈a✝¹⌉a✝