simp [voc,vocabOfFormula] at *
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ voc (⌈α⌉φ0)
⊢ repl_in_F x ρ (⌈α⌉φ0) = ⌈α⌉φ0
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α ∧ repl_in_F x ρ φ0 = φ0