cases φ
x : ℕ
φ ρ : Formula
x_notin_phi : x ∉ voc φ
⊢ repl_in_F x ρ φ = φ
case bottom
x : ℕ
ρ : Formula
x_notin_phi : x ∉ voc Formula.bottom
⊢ repl_in_F x ρ Formula.bottom = Formula.bottom

case atom_prop
x : ℕ
ρ : Formula
a✝ : ℕ
x_notin_phi : x ∉ voc (·a✝)
⊢ repl_in_F x ρ (·a✝) = ·a✝

case neg
x : ℕ
ρ a✝ : Formula
x_notin_phi : x ∉ voc (~a✝)
⊢ repl_in_F x ρ (~a✝) = (~a✝)

case and
x : ℕ
ρ a✝¹ a✝ : Formula
x_notin_phi : x ∉ voc (a✝¹⋀a✝)
⊢ repl_in_F x ρ (a✝¹⋀a✝) = a✝¹⋀a✝

case box
x : ℕ
ρ : Formula
a✝¹ : Program
a✝ : Formula
x_notin_phi : x ∉ voc (⌈a✝¹⌉a✝)
⊢ repl_in_F x ρ (⌈a✝¹⌉a✝) = ⌈a✝¹⌉a✝