all_goals simp [voc,vocabOfProgram] at *
case atom_prog
x : ℕ
ρ : Formula
a✝ : ℕ
x_notin_alpha : x ∉ voc (·a✝)
⊢ repl_in_P x ρ (·a✝) = ·a✝

case sequence
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ voc (a✝¹;'a✝)
⊢ repl_in_P x ρ (a✝¹;'a✝) = (a✝¹;'a✝)

case union
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ voc (a✝¹⋓a✝)
⊢ repl_in_P x ρ (a✝¹⋓a✝) = (a✝¹⋓a✝)

case star
x : ℕ
ρ : Formula
a✝ : Program
x_notin_alpha : x ∉ voc (∗a✝)
⊢ repl_in_P x ρ (∗a✝) = (∗a✝)

case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ voc (?'a✝)
⊢ repl_in_P x ρ (?'a✝) = (?'a✝)
case sequence
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
⊢ repl_in_P x ρ a✝¹ = a✝¹ ∧ repl_in_P x ρ a✝ = a✝

case union
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
⊢ repl_in_P x ρ a✝¹ = a✝¹ ∧ repl_in_P x ρ a✝ = a✝

case star
x : ℕ
ρ : Formula
a✝ : Program
x_notin_alpha : x ∉ vocabOfProgram a✝
⊢ repl_in_P x ρ a✝ = a✝

case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ vocabOfFormula a✝
⊢ repl_in_F x ρ a✝ = a✝