simp [voc,vocabOfProgram] at *
case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ voc (?'a✝)
⊢ repl_in_P x ρ (?'a✝) = (?'a✝)
case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ vocabOfFormula a✝
⊢ repl_in_F x ρ a✝ = a✝